Merge branch 'master' into MR-lint-lake-import

Mathlib/Algebra/GeomSum.lean

@@ -10,6 +10,7 @@ import Mathlib.Algebra.Order.Field.Basic
 import Mathlib.Algebra.Order.Ring.Abs
 import Mathlib.Algebra.Ring.Opposite
 import Mathlib.Tactic.Abel
+import Mathlib.Algebra.Ring.Regular
 
 #align_import algebra.geom_sum from "leanprover-community/mathlib"@"f7fc89d5d5ff1db2d1242c7bb0e9062ce47ef47c"
 

Mathlib/Algebra/Group/AddChar.lean

@@ -34,7 +34,7 @@ additive character
 ### Definitions related to and results on additive characters
 -/
 
-open Multiplicative
+open Function Multiplicative
 
 section AddCharDef
 
@@ -74,7 +74,7 @@ namespace AddChar
 section Basic
 -- results which don't require commutativity or inverses
 
-variable {A M : Type*} [AddMonoid A] [Monoid M]
+variable {A B M N : Type*} [AddMonoid A] [AddMonoid B] [Monoid M] [Monoid N] {ψ : AddChar A M}
 
 /-- Define coercion to a function. -/
 instance instFunLike : FunLike (AddChar A M) A M where
@@ -125,7 +125,6 @@ lemma map_nsmul_eq_pow (ψ : AddChar A M) (n : ℕ) (x : A) : ψ (n • x) = ψ
 
 @[deprecated (since := "2024-06-06")] alias map_nsmul_pow := map_nsmul_eq_pow
 
-variable (A M) in
 /-- Additive characters `A → M` are the same thing as monoid homomorphisms from `Multiplicative A`
 to `M`. -/
 def toMonoidHomEquiv : AddChar A M ≃ (Multiplicative A →* M) where
@@ -137,15 +136,29 @@ def toMonoidHomEquiv : AddChar A M ≃ (Multiplicative A →* M) where
   left_inv _ := rfl
   right_inv _ := rfl
 
+@[simp, norm_cast] lemma coe_toMonoidHomEquiv (ψ : AddChar A M) :
+    ⇑(toMonoidHomEquiv ψ) = ψ ∘ Multiplicative.toAdd := rfl
+
+@[simp, norm_cast] lemma coe_toMonoidHomEquiv_symm (ψ : Multiplicative A →* M) :
+    ⇑(toMonoidHomEquiv.symm ψ) = ψ ∘ Multiplicative.ofAdd := rfl
+
+@[simp] lemma toMonoidHomEquiv_apply (ψ : AddChar A M) (a : Multiplicative A) :
+    toMonoidHomEquiv ψ a = ψ (Multiplicative.toAdd a) := rfl
+
+@[simp] lemma toMonoidHomEquiv_symm_apply (ψ : Multiplicative A →* M) (a : A) :
+    toMonoidHomEquiv.symm ψ a = ψ (Multiplicative.ofAdd a) := rfl
+
 /-- Interpret an additive character as a monoid homomorphism. -/
 def toAddMonoidHom (φ : AddChar A M) : A →+ Additive M where
   toFun := φ.toFun
   map_zero' := φ.map_zero_eq_one'
   map_add' := φ.map_add_eq_mul'
 
-@[simp] lemma toAddMonoidHom_apply (ψ : AddChar A M) (a : A) : ψ.toAddMonoidHom a = ψ a := rfl
+@[simp] lemma coe_toAddMonoidHom (ψ : AddChar A M) : ⇑ψ.toAddMonoidHom = Additive.ofMul ∘ ψ := rfl
+
+@[simp] lemma toAddMonoidHom_apply (ψ : AddChar A M) (a : A) :
+    ψ.toAddMonoidHom a = Additive.ofMul (ψ a) := rfl
 
-variable (A M) in
 /-- Additive characters `A → M` are the same thing as additive homomorphisms from `A` to
 `Additive M`. -/
 def toAddMonoidHomEquiv : AddChar A M ≃ (A →+ Additive M) where
@@ -157,36 +170,78 @@ def toAddMonoidHomEquiv : AddChar A M ≃ (A →+ Additive M) where
   left_inv _ := rfl
   right_inv _ := rfl
 
+@[simp, norm_cast]
+lemma coe_toAddMonoidHomEquiv (ψ : AddChar A M) :
+    ⇑(toAddMonoidHomEquiv ψ) = Additive.ofMul ∘ ψ := rfl
+
+@[simp, norm_cast] lemma coe_toAddMonoidHomEquiv_symm (ψ : A →+ Additive M) :
+    ⇑(toAddMonoidHomEquiv.symm ψ) = Additive.toMul ∘ ψ := rfl
+
+@[simp] lemma toAddMonoidHomEquiv_apply (ψ : AddChar A M) (a : A) :
+    toAddMonoidHomEquiv ψ a = Additive.ofMul (ψ a) := rfl
+
+@[simp] lemma toAddMonoidHomEquiv_symm_apply (ψ : A →+ Additive M) (a : A) :
+    toAddMonoidHomEquiv.symm ψ a = Additive.toMul (ψ a) := rfl
+
 /-- The trivial additive character (sending everything to `1`) is `(1 : AddChar A M).` -/
-instance instOne : One (AddChar A M) := (toMonoidHomEquiv A M).one
+instance instOne : One (AddChar A M) := toMonoidHomEquiv.one
 
--- Porting note: added
+@[simp, norm_cast] lemma coe_one : ⇑(1 : AddChar A M) = 1 := rfl
 @[simp] lemma one_apply (a : A) : (1 : AddChar A M) a = 1 := rfl
 
 instance instInhabited : Inhabited (AddChar A M) := ⟨1⟩
 
 /-- Composing a `MonoidHom` with an `AddChar` yields another `AddChar`. -/
 def _root_.MonoidHom.compAddChar {N : Type*} [Monoid N] (f : M →* N) (φ : AddChar A M) :
-    AddChar A N :=
-  (toMonoidHomEquiv A N).symm (f.comp φ.toMonoidHom)
+    AddChar A N := toMonoidHomEquiv.symm (f.comp φ.toMonoidHom)
 
-@[simp]
+@[simp, norm_cast]
 lemma _root_.MonoidHom.coe_compAddChar {N : Type*} [Monoid N] (f : M →* N) (φ : AddChar A M) :
     f.compAddChar φ = f ∘ φ :=
   rfl
 
+@[simp, norm_cast]
+lemma _root_.MonoidHom.compAddChar_apply (f : M →* N) (φ : AddChar A M) : f.compAddChar φ = f ∘ φ :=
+  rfl
+
+lemma _root_.MonoidHom.compAddChar_injective_left (ψ : AddChar A M) (hψ : Surjective ψ) :
+    Injective fun f : M →* N ↦ f.compAddChar ψ := by
+  rintro f g h; rw [DFunLike.ext'_iff] at h ⊢; exact hψ.injective_comp_right h
+
+lemma _root_.MonoidHom.compAddChar_injective_right (f : M →* N) (hf : Injective f) :
+    Injective fun ψ : AddChar B M ↦ f.compAddChar ψ := by
+  rintro ψ χ h; rw [DFunLike.ext'_iff] at h ⊢; exact hf.comp_left h
+
 /-- Composing an `AddChar` with an `AddMonoidHom` yields another `AddChar`. -/
-def compAddMonoidHom {B : Type*} [AddMonoid B] (φ : AddChar B M) (f : A →+ B) : AddChar A M :=
-  (toAddMonoidHomEquiv A M).symm (φ.toAddMonoidHom.comp f)
+def compAddMonoidHom (φ : AddChar B M) (f : A →+ B) : AddChar A M :=
+  toAddMonoidHomEquiv.symm (φ.toAddMonoidHom.comp f)
+
+@[simp, norm_cast]
+lemma coe_compAddMonoidHom (φ : AddChar B M) (f : A →+ B) : φ.compAddMonoidHom f = φ ∘ f := rfl
+
+@[simp] lemma compAddMonoidHom_apply (ψ : AddChar B M) (f : A →+ B)
+    (a : A) : ψ.compAddMonoidHom f a = ψ (f a) := rfl
+
+lemma compAddMonoidHom_injective_left (f : A →+ B) (hf : Surjective f) :
+    Injective fun ψ : AddChar B M ↦ ψ.compAddMonoidHom f := by
+  rintro ψ χ h; rw [DFunLike.ext'_iff] at h ⊢; exact hf.injective_comp_right h
 
-@[simp] lemma coe_compAddMonoidHom {B : Type*} [AddMonoid B] (φ : AddChar B M) (f : A →+ B) :
-    φ.compAddMonoidHom f = φ ∘ f := rfl
+lemma compAddMonoidHom_injective_right (ψ : AddChar B M) (hψ : Injective ψ) :
+    Injective fun f : A →+ B ↦ ψ.compAddMonoidHom f := by
+  rintro f g h
+  rw [DFunLike.ext'_iff] at h ⊢; exact hψ.comp_left h
+
+lemma eq_one_iff : ψ = 1 ↔ ∀ x, ψ x = 1 := DFunLike.ext_iff
+lemma ne_one_iff : ψ ≠ 1 ↔ ∃ x, ψ x ≠ 1 := DFunLike.ne_iff
 
 /-- An additive character is *nontrivial* if it takes a value `≠ 1`. -/
+@[deprecated (since := "2024-06-06")]
 def IsNontrivial (ψ : AddChar A M) : Prop := ∃ a : A, ψ a ≠ 1
 #align add_char.is_nontrivial AddChar.IsNontrivial
 
+set_option linter.deprecated false in
 /-- An additive character is nontrivial iff it is not the trivial character. -/
+@[deprecated ne_one_iff (since := "2024-06-06")]
 lemma isNontrivial_iff_ne_trivial (ψ : AddChar A M) : IsNontrivial ψ ↔ ψ ≠ 1 :=
   not_forall.symm.trans (DFunLike.ext_iff (f := ψ) (g := 1)).symm.not
 
@@ -199,23 +254,21 @@ section toCommMonoid
 variable {A M : Type*} [AddMonoid A] [CommMonoid M]
 
 /-- When `M` is commutative, `AddChar A M` is a commutative monoid. -/
-instance instCommMonoid : CommMonoid (AddChar A M) := (toMonoidHomEquiv A M).commMonoid
-
--- Porting note: added
-@[simp] lemma mul_apply (ψ φ : AddChar A M) (a : A) : (ψ * φ) a = ψ a * φ a := rfl
-
-@[simp] lemma pow_apply (ψ : AddChar A M) (n : ℕ) (a : A) : (ψ ^ n) a = (ψ a) ^ n := rfl
+instance instCommMonoid : CommMonoid (AddChar A M) := toMonoidHomEquiv.commMonoid
 
-variable (A M)
+@[simp, norm_cast] lemma coe_mul (ψ χ : AddChar A M) : ⇑(ψ * χ) = ψ * χ := rfl
+@[simp, norm_cast] lemma coe_pow (ψ : AddChar A M) (n : ℕ) : ⇑(ψ ^ n) = ψ ^ n := rfl
+@[simp, norm_cast] lemma mul_apply (ψ φ : AddChar A M) (a : A) : (ψ * φ) a = ψ a * φ a := rfl
+@[simp, norm_cast] lemma pow_apply (ψ : AddChar A M) (n : ℕ) (a : A) : (ψ ^ n) a = (ψ a) ^ n := rfl
 
 /-- The natural equivalence to `(Multiplicative A →* M)` is a monoid isomorphism. -/
 def toMonoidHomMulEquiv : AddChar A M ≃* (Multiplicative A →* M) :=
-  { toMonoidHomEquiv A M with map_mul' := fun φ ψ ↦ by rfl }
+  { toMonoidHomEquiv with map_mul' := fun φ ψ ↦ by rfl }
 
 /-- Additive characters `A → M` are the same thing as additive homomorphisms from `A` to
 `Additive M`. -/
 def toAddMonoidAddEquiv : Additive (AddChar A M) ≃+ (A →+ Additive M) :=
-  { toAddMonoidHomEquiv A M with map_add' := fun φ ψ ↦ by rfl }
+  { toAddMonoidHomEquiv with map_add' := fun φ ψ ↦ by rfl }
 
 end toCommMonoid
 
@@ -275,6 +328,12 @@ variable {A M : Type*} [AddCommGroup A] [DivisionCommMonoid M]
 
 lemma inv_apply' (ψ : AddChar A M) (x : A) : ψ⁻¹ x = (ψ x)⁻¹ := by rw [inv_apply, map_neg_eq_inv]
 
+lemma map_sub_eq_div (ψ : AddChar A M) (a b : A) : ψ (a - b) = ψ a / ψ b :=
+  ψ.toMonoidHom.map_div _ _
+
+lemma injective_iff {ψ : AddChar A M} : Injective ψ ↔ ∀ ⦃x⦄, ψ x = 1 → x = 0 :=
+  ψ.toMonoidHom.ker_eq_bot_iff.symm.trans eq_bot_iff
+
 end fromAddGrouptoDivisionCommMonoid
 
 /-!

Mathlib/Algebra/Order/AbsoluteValue.lean

@@ -7,7 +7,7 @@ import Mathlib.Algebra.GroupWithZero.Units.Lemmas
 import Mathlib.Algebra.Order.Field.Defs
 import Mathlib.Algebra.Order.Hom.Basic
 import Mathlib.Algebra.Order.Ring.Abs
-import Mathlib.Algebra.Ring.Regular
+import Mathlib.Algebra.Regular.Basic
 
 #align_import algebra.order.absolute_value from "leanprover-community/mathlib"@"0013240bce820e3096cebb7ccf6d17e3f35f77ca"
 

Mathlib/Algebra/Regular/Basic.lean

@@ -375,11 +375,11 @@ theorem IsRegular.all [Mul R] [IsCancelMul R] (g : R) : IsRegular g :=
 
 section CancelMonoidWithZero
 
-variable [CancelMonoidWithZero R] {a : R}
+variable [MulZeroClass R] [IsCancelMulZero R] {a : R} {a : R}
 
 /-- Non-zero elements of an integral domain are regular. -/
 theorem isRegular_of_ne_zero (a0 : a ≠ 0) : IsRegular a :=
-  ⟨fun _ _ => (mul_right_inj' a0).mp, fun _ _ => (mul_left_inj' a0).mp⟩
+  ⟨fun _ _ => mul_left_cancel₀ a0, fun _ _ => mul_right_cancel₀ a0⟩
 #align is_regular_of_ne_zero isRegular_of_ne_zero
 
 /-- In a non-trivial integral domain, an element is regular iff it is non-zero. -/

Mathlib/Algebra/Ring/Basic.lean

@@ -149,7 +149,7 @@ section NoZeroDivisors
 
 variable (α)
 
-lemma IsLeftCancelMulZero.to_noZeroDivisors [Ring α] [IsLeftCancelMulZero α] :
+lemma IsLeftCancelMulZero.to_noZeroDivisors [NonUnitalNonAssocRing α] [IsLeftCancelMulZero α] :
     NoZeroDivisors α :=
   { eq_zero_or_eq_zero_of_mul_eq_zero := fun {x y} h ↦ by
       by_cases hx : x = 0
@@ -161,7 +161,7 @@ lemma IsLeftCancelMulZero.to_noZeroDivisors [Ring α] [IsLeftCancelMulZero α] :
         rwa [sub_zero] at this } }
 #align is_left_cancel_mul_zero.to_no_zero_divisors IsLeftCancelMulZero.to_noZeroDivisors
 
-lemma IsRightCancelMulZero.to_noZeroDivisors [Ring α] [IsRightCancelMulZero α] :
+lemma IsRightCancelMulZero.to_noZeroDivisors [NonUnitalNonAssocRing α] [IsRightCancelMulZero α] :
     NoZeroDivisors α :=
   { eq_zero_or_eq_zero_of_mul_eq_zero := fun {x y} h ↦ by
       by_cases hy : y = 0
@@ -173,7 +173,8 @@ lemma IsRightCancelMulZero.to_noZeroDivisors [Ring α] [IsRightCancelMulZero α]
         rwa [sub_zero] at this } }
 #align is_right_cancel_mul_zero.to_no_zero_divisors IsRightCancelMulZero.to_noZeroDivisors
 
-instance (priority := 100) NoZeroDivisors.to_isCancelMulZero [Ring α] [NoZeroDivisors α] :
+instance (priority := 100) NoZeroDivisors.to_isCancelMulZero
+    [NonUnitalNonAssocRing α] [NoZeroDivisors α] :
     IsCancelMulZero α :=
   { mul_left_cancel_of_ne_zero := fun ha h ↦ by
       rw [← sub_eq_zero, ← mul_sub] at h
@@ -184,7 +185,7 @@ instance (priority := 100) NoZeroDivisors.to_isCancelMulZero [Ring α] [NoZeroDi
 #align no_zero_divisors.to_is_cancel_mul_zero NoZeroDivisors.to_isCancelMulZero
 
 /-- In a ring, `IsCancelMulZero` and `NoZeroDivisors` are equivalent. -/
-lemma isCancelMulZero_iff_noZeroDivisors [Ring α] :
+lemma isCancelMulZero_iff_noZeroDivisors [NonUnitalNonAssocRing α] :
     IsCancelMulZero α ↔ NoZeroDivisors α :=
   ⟨fun _ => IsRightCancelMulZero.to_noZeroDivisors _, fun _ => inferInstance⟩
 

Mathlib/Data/Real/NNReal.lean

@@ -11,6 +11,7 @@ import Mathlib.Algebra.Order.Nonneg.Floor
 import Mathlib.Data.Real.Pointwise
 import Mathlib.Order.ConditionallyCompleteLattice.Group
 import Mathlib.Tactic.GCongr.Core
+import Mathlib.Algebra.Ring.Regular
 
 #align_import data.real.nnreal from "leanprover-community/mathlib"@"b1abe23ae96fef89ad30d9f4362c307f72a55010"
 

Mathlib/NumberTheory/GaussSum.lean

@@ -92,7 +92,7 @@ variable {R : Type u} [Field R] [Fintype R] {R' : Type v} [CommRing R'] [IsDomai
 
 -- A helper lemma for `gaussSum_mul_gaussSum_eq_card` below
 -- Is this useful enough in other contexts to be public?
-private theorem gaussSum_mul_aux {χ : MulChar R R'} (hχ : IsNontrivial χ) (ψ : AddChar R R')
+private theorem gaussSum_mul_aux {χ : MulChar R R'} (hχ : χ.IsNontrivial) (ψ : AddChar R R')
     (b : R) : ∑ a, χ (a * b⁻¹) * ψ (a - b) = ∑ c, χ c * ψ (b * (c - 1)) := by
   rcases eq_or_ne b 0 with hb | hb
   · -- case `b = 0`
@@ -105,7 +105,7 @@ private theorem gaussSum_mul_aux {χ : MulChar R R'} (hχ : IsNontrivial χ) (ψ
 
 /-- We have `gaussSum χ ψ * gaussSum χ⁻¹ ψ⁻¹ = Fintype.card R`
 when `χ` is nontrivial and `ψ` is primitive (and `R` is a field). -/
-theorem gaussSum_mul_gaussSum_eq_card {χ : MulChar R R'} (hχ : IsNontrivial χ) {ψ : AddChar R R'}
+theorem gaussSum_mul_gaussSum_eq_card {χ : MulChar R R'} (hχ : χ.IsNontrivial) {ψ : AddChar R R'}
     (hψ : IsPrimitive ψ) : gaussSum χ ψ * gaussSum χ⁻¹ ψ⁻¹ = Fintype.card R := by
   simp only [gaussSum, AddChar.inv_apply, Finset.sum_mul, Finset.mul_sum, MulChar.inv_apply']
   conv =>
@@ -124,7 +124,7 @@ theorem gaussSum_mul_gaussSum_eq_card {χ : MulChar R R'} (hχ : IsNontrivial χ
 
 /-- When `χ` is a nontrivial quadratic character, then the square of `gaussSum χ ψ`
 is `χ(-1)` times the cardinality of `R`. -/
-theorem gaussSum_sq {χ : MulChar R R'} (hχ₁ : IsNontrivial χ) (hχ₂ : IsQuadratic χ)
+theorem gaussSum_sq {χ : MulChar R R'} (hχ₁ : χ.IsNontrivial) (hχ₂ : IsQuadratic χ)
     {ψ : AddChar R R'} (hψ : IsPrimitive ψ) : gaussSum χ ψ ^ 2 = χ (-1) * Fintype.card R := by
   rw [pow_two, ← gaussSum_mul_gaussSum_eq_card hχ₁ hψ, hχ₂.inv, mul_rotate']
   congr
@@ -209,7 +209,7 @@ theorem Char.card_pow_char_pow {χ : MulChar R R'} (hχ : IsQuadratic χ) (ψ :
 /-- When `F` and `F'` are finite fields and `χ : F → F'` is a nontrivial quadratic character,
 then `(χ(-1) * #F)^(#F'/2) = χ(#F')`. -/
 theorem Char.card_pow_card {F : Type*} [Field F] [Fintype F] {F' : Type*} [Field F'] [Fintype F']
-    {χ : MulChar F F'} (hχ₁ : IsNontrivial χ) (hχ₂ : IsQuadratic χ)
+    {χ : MulChar F F'} (hχ₁ : χ.IsNontrivial) (hχ₂ : IsQuadratic χ)
     (hch₁ : ringChar F' ≠ ringChar F) (hch₂ : ringChar F' ≠ 2) :
     (χ (-1) * Fintype.card F) ^ (Fintype.card F' / 2) = χ (Fintype.card F') := by
   obtain ⟨n, hp, hc⟩ := FiniteField.card F (ringChar F)