chore(algebra/group): rename is_unit_unit to units.is_unit (#6886)

src/algebra/group/units.lean

@@ -236,7 +236,7 @@ def is_unit [monoid M] (a : M) : Prop := ∃ u : units M, (u : M) = a
 ⟨⟨a, a, subsingleton.elim _ _, subsingleton.elim _ _⟩, rfl⟩
 
 @[simp, to_additive is_add_unit_add_unit]
-lemma is_unit_unit [monoid M] (u : units M) : is_unit (u : M) := ⟨u, rfl⟩
+protected lemma units.is_unit [monoid M] (u : units M) : is_unit (u : M) := ⟨u, rfl⟩
 
 @[simp, to_additive is_add_unit_zero]
 theorem is_unit_one [monoid M] : is_unit (1:M) := ⟨1, rfl⟩

src/algebra/group/units_hom.lean

@@ -92,7 +92,7 @@ variables {M : Type*} {N : Type*}
 
 @[to_additive] lemma is_unit.map [monoid M] [monoid N]
   (f : M →* N) {x : M} (h : is_unit x) : is_unit (f x) :=
-by rcases h with ⟨y, rfl⟩; exact is_unit_unit (units.map f y)
+by rcases h with ⟨y, rfl⟩; exact (units.map f y).is_unit
 
 /-- If a homomorphism `f : M →* N` sends each element to an `is_unit`, then it can be lifted
 to `f : M →* units N`. See also `units.lift_right` for a computable version. -/

src/algebra/group_with_zero/basic.lean

@@ -512,7 +512,7 @@ end units
 section group_with_zero
 variables [group_with_zero G₀]
 
-lemma is_unit.mk0 (x : G₀) (hx : x ≠ 0) : is_unit x := is_unit_unit (units.mk0 x hx)
+lemma is_unit.mk0 (x : G₀) (hx : x ≠ 0) : is_unit x := (units.mk0 x hx).is_unit
 
 lemma is_unit_iff_ne_zero {x : G₀} : is_unit x ↔ x ≠ 0 :=
 units.exists_iff_ne_zero

src/algebra/ring/basic.lean

@@ -921,8 +921,8 @@ noncomputable def inverse : M₀ → M₀ :=
 /-- By definition, if `x` is invertible then `inverse x = x⁻¹`. -/
 @[simp] lemma inverse_unit (u : units M₀) : inverse (u : M₀) = (u⁻¹ : units M₀) :=
 begin
-  simp only [is_unit_unit, inverse, dif_pos],
-  exact units.inv_unique (classical.some_spec (is_unit_unit u))
+  simp only [units.is_unit, inverse, dif_pos],
+  exact units.inv_unique (classical.some_spec u.is_unit)
 end
 
 /-- By definition, if `x` is not invertible then `inverse x = 0`. -/

src/analysis/normed_space/units.lean

@@ -82,7 +82,7 @@ begin
 end
 
 protected lemma nhds (x : units R) : {x : R | is_unit x} ∈ 𝓝 (x : R) :=
-mem_nhds_sets units.is_open (is_unit_unit x)
+mem_nhds_sets units.is_open x.is_unit
 
 end units
 

src/data/equiv/mul_add.lean

@@ -362,7 +362,7 @@ def to_units {G} [group G] : G ≃* units G :=
   right_inv := λ u, units.ext rfl,
   map_mul' := λ x y, units.ext rfl }
 
-protected lemma group.is_unit {G} [group G] (x : G) : is_unit x := is_unit_unit (to_units x)
+protected lemma group.is_unit {G} [group G] (x : G) : is_unit x := (to_units x).is_unit
 
 namespace units
 

src/data/padics/padic_integers.lean

@@ -500,7 +500,7 @@ begin
     contrapose! hx, rw [hx, mul_zero], },
   { rw [unit_coeff_spec hx] { occs := occurrences.pos [2] },
     lift x.valuation to ℕ using x.valuation_nonneg with k hk,
-    simp only [int.nat_abs_of_nat, is_unit_unit, is_unit.dvd_mul_left, int.coe_nat_le],
+    simp only [int.nat_abs_of_nat, units.is_unit, is_unit.dvd_mul_left, int.coe_nat_le],
     intro H,
     obtain ⟨k, rfl⟩ := nat.exists_eq_add_of_le H,
     simp only [pow_add, dvd_mul_right], }

src/dynamics/circle/rotation_number/translation_number.lean

@@ -206,7 +206,7 @@ def to_order_iso : units circle_deg1_lift →* ℝ ≃o ℝ :=
   ⇑(to_order_iso f)⁻¹ = (f⁻¹ : units circle_deg1_lift) := rfl
 
 lemma is_unit_iff_bijective {f : circle_deg1_lift} : is_unit f ↔ bijective f :=
-⟨λ ⟨u, h⟩, h ▸ (to_order_iso u).bijective, λ h, is_unit_unit
+⟨λ ⟨u, h⟩, h ▸ (to_order_iso u).bijective, λ h, units.is_unit
   { val := f,
     inv := { to_fun := (equiv.of_bijective f h).symm,
              monotone' := λ x y hxy, (f.strict_mono_iff_injective.2 h.1).le_iff_le.1

src/linear_algebra/nonsingular_inverse.lean

@@ -348,7 +348,7 @@ begin
     { rcases this with ⟨B, hB⟩, apply is_unit_of_mul_eq_one _ B.det, rw [←det_mul, hB, det_one], },
     refine ⟨↑h.unit⁻¹, _⟩, conv_lhs { congr, rw ←h.unit_spec, }, exact h.unit.mul_inv, },
   { -- is_unit A.det → is_unit A
-    exact is_unit_unit (A.nonsing_inv_unit h), },
+    exact (A.nonsing_inv_unit h).is_unit, },
 end
 
 lemma is_unit_det_of_left_inverse (B : matrix n n α) (h : B ⬝ A = 1) : is_unit A.det :=

src/ring_theory/discrete_valuation_ring.lean

@@ -195,8 +195,8 @@ begin
     by_cases hb : b = 0,
     { rw hb, simp only [or_true, dvd_zero], },
     obtain ⟨m, u, rfl⟩ := spec.2 ha,
-    rw [mul_assoc, mul_left_comm, is_unit.dvd_mul_left _ _ _ (is_unit_unit _)] at h,
-    rw is_unit.dvd_mul_right (is_unit_unit _),
+    rw [mul_assoc, mul_left_comm, is_unit.dvd_mul_left _ _ _ (units.is_unit _)] at h,
+    rw is_unit.dvd_mul_right (units.is_unit _),
     by_cases hm : m = 0,
     { simp only [hm, one_mul, pow_zero] at h ⊢, right, exact h },
     left,
@@ -256,7 +256,7 @@ begin
     by_cases hr0 : r = 0,
     { simp only [hr0, submodule.zero_mem], },
     obtain ⟨n, u, rfl⟩ := H hr0,
-    simp only [mem_span_singleton, is_unit_unit, is_unit.dvd_mul_right],
+    simp only [mem_span_singleton, units.is_unit, is_unit.dvd_mul_right],
     apply pow_dvd_pow,
     apply nat.find_min',
     simpa only [units.mul_inv_cancel_right] using I.mul_mem_right ↑u⁻¹ hr, },

src/ring_theory/multiplicity.lean

@@ -136,10 +136,10 @@ get_eq_iff_eq_some.2 (eq_some_iff.2 ⟨dvd_refl _,
   by simpa [is_unit_iff_dvd_one.symm] using not_unit_of_finite ha⟩)
 
 @[simp] lemma unit_left (a : α) (u : units α) : multiplicity (u : α) a = ⊤ :=
-is_unit_left a (is_unit_unit u)
+is_unit_left a u.is_unit
 
 lemma unit_right {a : α} (ha : ¬is_unit a) (u : units α) : multiplicity a u = 0 :=
-is_unit_right ha (is_unit_unit u)
+is_unit_right ha u.is_unit
 
 lemma multiplicity_eq_zero_of_not_dvd {a b : α} (ha : ¬a ∣ b) : multiplicity a b = 0 :=
 eq_some_iff.2 (by simpa)

src/ring_theory/power_series/basic.lean

@@ -656,7 +656,7 @@ instance map.is_local_ring_hom : is_local_ring_hom (map σ f) :=
   rintros φ ⟨ψ, h⟩,
   replace h := congr_arg (constant_coeff σ S) h,
   rw constant_coeff_map at h,
-  have : is_unit (constant_coeff σ S ↑ψ) := @is_unit_constant_coeff σ S _ (↑ψ) (is_unit_unit ψ),
+  have : is_unit (constant_coeff σ S ↑ψ) := @is_unit_constant_coeff σ S _ (↑ψ) ψ.is_unit,
   rw h at this,
   rcases is_unit_of_map_unit f _ this with ⟨c, hc⟩,
   exact is_unit_of_mul_eq_one φ (inv_of_unit φ c) (mul_inv_of_unit φ c hc.symm)