Skip to content

Commit e652730

Browse files
BryceT233ReemMelamed
authored andcommitted
chore(Algebra/Ring/Subring/Units): remove an unused variable (leanprover-community#40169)
In leanprover-community#40152, I accidentally left an unused variable in the statement; this PR removes it
1 parent db51029 commit e652730

1 file changed

Lines changed: 2 additions & 3 deletions

File tree

Mathlib/Algebra/Ring/Subring/Units.lean

Lines changed: 2 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -31,9 +31,8 @@ theorem Units.mem_posSubgroup {R : Type*} [Semiring R] [LinearOrder R] [IsStrict
3131
(u : Rˣ) : u ∈ Units.posSubgroup R ↔ (0 : R) < u :=
3232
Iff.rfl
3333

34-
theorem RingHom.isUnit_eqLocus_mk_iff {R S T : Type*} [Ring R] [Ring S] [Semiring T]
35-
(f g : R →+* T) {r : R} (hr : f r = g r) :
36-
IsUnit (⟨r, hr⟩ : f.eqLocus g) ↔ IsUnit r := by
34+
theorem RingHom.isUnit_eqLocus_mk_iff {R T : Type*} [Ring R] [Semiring T] (f g : R →+* T)
35+
{r : R} (hr : f r = g r) : IsUnit (⟨r, hr⟩ : f.eqLocus g) ↔ IsUnit r := by
3736
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
3837
· simp [isUnit_iff_exists, ← Subtype.val_inj] at h ⊢
3938
grind

0 commit comments

Comments
 (0)