chore(algebra): generalize typeclass arguments from field to semifield (#18597)

YaelDillies · eric-wieser · YaelDillies · commit 30413fc89f20 · 2023-03-17T09:39:09.000Z
This generalizes some typeclass arguments from `field` to `semifield` and `division_ring` to `division_semiring`. The proof for `map_inv_nat_cast_smul` had to be rewritten, as it was previously proved in terms of `map_inv_int_cast_smul`. The latter is now instead proved in terms of the former. Forward-ported in leanprover-community/mathlib4#2926 Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
diff --git a/src/algebra/module/basic.lean b/src/algebra/module/basic.lean
@@ -381,27 +381,32 @@ lemma map_nat_cast_smul [add_comm_monoid M] [add_comm_monoid M₂] {F : Type*}
   f ((x : R) • a) = (x : S) • f a :=
 by simp only [←nsmul_eq_smul_cast, map_nsmul]
 
-lemma map_inv_int_cast_smul [add_comm_group M] [add_comm_group M₂] {F : Type*}
+lemma map_inv_nat_cast_smul [add_comm_monoid M] [add_comm_monoid M₂] {F : Type*}
   [add_monoid_hom_class F M M₂] (f : F)
-  (R S : Type*) [division_ring R] [division_ring S] [module R M] [module S M₂]
-  (n : ℤ) (x : M) :
+  (R S : Type*) [division_semiring R] [division_semiring S] [module R M] [module S M₂]
+  (n : ℕ) (x : M) :
   f ((n⁻¹ : R) • x) = (n⁻¹ : S) • f x :=
 begin
   by_cases hR : (n : R) = 0; by_cases hS : (n : S) = 0,
   { simp [hR, hS] },
   { suffices : ∀ y, f y = 0, by simp [this], clear x, intro x,
-    rw [← inv_smul_smul₀ hS (f x), ← map_int_cast_smul f R S], simp [hR] },
+    rw [← inv_smul_smul₀ hS (f x), ← map_nat_cast_smul f R S], simp [hR] },
   { suffices : ∀ y, f y = 0, by simp [this], clear x, intro x,
-    rw [← smul_inv_smul₀ hR x, map_int_cast_smul f R S, hS, zero_smul] },
-  { rw [← inv_smul_smul₀ hS (f _), ← map_int_cast_smul f R S, smul_inv_smul₀ hR] }
+    rw [← smul_inv_smul₀ hR x, map_nat_cast_smul f R S, hS, zero_smul] },
+  { rw [← inv_smul_smul₀ hS (f _), ← map_nat_cast_smul f R S, smul_inv_smul₀ hR] }
 end
 
-lemma map_inv_nat_cast_smul [add_comm_group M] [add_comm_group M₂] {F : Type*}
+lemma map_inv_int_cast_smul [add_comm_group M] [add_comm_group M₂] {F : Type*}
   [add_monoid_hom_class F M M₂] (f : F)
   (R S : Type*) [division_ring R] [division_ring S] [module R M] [module S M₂]
-  (n : ℕ) (x : M) :
-  f ((n⁻¹ : R) • x) = (n⁻¹ : S) • f x :=
-by exact_mod_cast map_inv_int_cast_smul f R S n x
+  (z : ℤ) (x : M) :
+  f ((z⁻¹ : R) • x) = (z⁻¹ : S) • f x :=
+begin
+  obtain ⟨n, rfl | rfl⟩ := z.eq_coe_or_neg,
+  { rw [int.cast_coe_nat, int.cast_coe_nat, map_inv_nat_cast_smul _ R S] },
+  { simp_rw [int.cast_neg, int.cast_coe_nat, inv_neg, neg_smul, map_neg,
+      map_inv_nat_cast_smul _ R S] },
+end
 
 lemma map_rat_cast_smul [add_comm_group M] [add_comm_group M₂] {F : Type*}
   [add_monoid_hom_class F M M₂] (f : F)
@@ -421,34 +426,34 @@ instance subsingleton_rat_module (E : Type*) [add_comm_group E] : subsingleton (
 ⟨λ P Q, module.ext' P Q $ λ r x,
   @map_rat_smul _ _ _ _ P Q _ _ (add_monoid_hom.id E) r x⟩
 
+/-- If `E` is a vector space over two division semirings `R` and `S`, then scalar multiplications
+agree on inverses of natural numbers in `R` and `S`. -/
+lemma inv_nat_cast_smul_eq {E : Type*} (R S : Type*) [add_comm_monoid E] [division_semiring R]
+  [division_semiring S] [module R E] [module S E] (n : ℕ) (x : E) :
+  (n⁻¹ : R) • x = (n⁻¹ : S) • x :=
+map_inv_nat_cast_smul (add_monoid_hom.id E) R S n x
+
 /-- If `E` is a vector space over two division rings `R` and `S`, then scalar multiplications
 agree on inverses of integer numbers in `R` and `S`. -/
 lemma inv_int_cast_smul_eq {E : Type*} (R S : Type*) [add_comm_group E] [division_ring R]
   [division_ring S] [module R E] [module S E] (n : ℤ) (x : E) :
   (n⁻¹ : R) • x = (n⁻¹ : S) • x :=
 map_inv_int_cast_smul (add_monoid_hom.id E) R S n x
 
-/-- If `E` is a vector space over two division rings `R` and `S`, then scalar multiplications
-agree on inverses of natural numbers in `R` and `S`. -/
-lemma inv_nat_cast_smul_eq {E : Type*} (R S : Type*) [add_comm_group E] [division_ring R]
-  [division_ring S] [module R E] [module S E] (n : ℕ) (x : E) :
-  (n⁻¹ : R) • x = (n⁻¹ : S) • x :=
-map_inv_nat_cast_smul (add_monoid_hom.id E) R S n x
+/-- If `E` is a vector space over a division ring `R` and has a monoid action by `α`, then that
+action commutes by scalar multiplication of inverses of natural numbers in `R`. -/
+lemma inv_nat_cast_smul_comm {α E : Type*} (R : Type*) [add_comm_monoid E] [division_semiring R]
+  [monoid α] [module R E] [distrib_mul_action α E] (n : ℕ) (s : α) (x : E) :
+  (n⁻¹ : R) • s • x = s • (n⁻¹ : R) • x :=
+(map_inv_nat_cast_smul (distrib_mul_action.to_add_monoid_hom E s) R R n x).symm
 
-/-- If `E` is a vector space over a division rings `R` and has a monoid action by `α`, then that
+/-- If `E` is a vector space over a division ring `R` and has a monoid action by `α`, then that
 action commutes by scalar multiplication of inverses of integers in `R` -/
 lemma inv_int_cast_smul_comm {α E : Type*} (R : Type*) [add_comm_group E] [division_ring R]
   [monoid α] [module R E] [distrib_mul_action α E] (n : ℤ) (s : α) (x : E) :
   (n⁻¹ : R) • s • x = s • (n⁻¹ : R) • x :=
 (map_inv_int_cast_smul (distrib_mul_action.to_add_monoid_hom E s) R R n x).symm
 
-/-- If `E` is a vector space over a division rings `R` and has a monoid action by `α`, then that
-action commutes by scalar multiplication of inverses of natural numbers in `R`. -/
-lemma inv_nat_cast_smul_comm {α E : Type*} (R : Type*) [add_comm_group E] [division_ring R]
-  [monoid α] [module R E] [distrib_mul_action α E] (n : ℕ) (s : α) (x : E) :
-  (n⁻¹ : R) • s • x = s • (n⁻¹ : R) • x :=
-(map_inv_nat_cast_smul (distrib_mul_action.to_add_monoid_hom E s) R R n x).symm
-
 /-- If `E` is a vector space over two division rings `R` and `S`, then scalar multiplications
 agree on rational numbers in `R` and `S`. -/
 lemma rat_cast_smul_eq {E : Type*} (R S : Type*) [add_comm_group E] [division_ring R]
diff --git a/src/algebra/periodic.lean b/src/algebra/periodic.lean
@@ -103,7 +103,7 @@ protected lemma periodic.const_smul [add_monoid α] [group γ] [distrib_mul_acti
   periodic (λ x, f (a • x)) (a⁻¹ • c) :=
 λ x, by simpa only [smul_add, smul_inv_smul] using h (a • x)
 
-lemma periodic.const_smul₀ [add_comm_monoid α] [division_ring γ] [module γ α]
+lemma periodic.const_smul₀ [add_comm_monoid α] [division_semiring γ] [module γ α]
   (h : periodic f c) (a : γ) :
   periodic (λ x, f (a • x)) (a⁻¹ • c) :=
 begin
@@ -112,7 +112,7 @@ begin
   simpa only [smul_add, smul_inv_smul₀ ha] using h (a • x),
 end
 
-protected lemma periodic.const_mul [division_ring α] (h : periodic f c) (a : α) :
+protected lemma periodic.const_mul [division_semiring α] (h : periodic f c) (a : α) :
   periodic (λ x, f (a * x)) (a⁻¹ * c) :=
 h.const_smul₀ a
 
@@ -121,29 +121,29 @@ lemma periodic.const_inv_smul [add_monoid α] [group γ] [distrib_mul_action γ
   periodic (λ x, f (a⁻¹ • x)) (a • c) :=
 by simpa only [inv_inv] using h.const_smul a⁻¹
 
-lemma periodic.const_inv_smul₀ [add_comm_monoid α] [division_ring γ] [module γ α]
+lemma periodic.const_inv_smul₀ [add_comm_monoid α] [division_semiring γ] [module γ α]
   (h : periodic f c) (a : γ) :
   periodic (λ x, f (a⁻¹ • x)) (a • c) :=
 by simpa only [inv_inv] using h.const_smul₀ a⁻¹
 
-lemma periodic.const_inv_mul [division_ring α] (h : periodic f c) (a : α) :
+lemma periodic.const_inv_mul [division_semiring α] (h : periodic f c) (a : α) :
   periodic (λ x, f (a⁻¹ * x)) (a * c) :=
 h.const_inv_smul₀ a
 
-lemma periodic.mul_const [division_ring α] (h : periodic f c) (a : α) :
+lemma periodic.mul_const [division_semiring α] (h : periodic f c) (a : α) :
   periodic (λ x, f (x * a)) (c * a⁻¹) :=
 h.const_smul₀ $ mul_opposite.op a
 
-lemma periodic.mul_const' [division_ring α]
+lemma periodic.mul_const' [division_semiring α]
   (h : periodic f c) (a : α) :
   periodic (λ x, f (x * a)) (c / a) :=
 by simpa only [div_eq_mul_inv] using h.mul_const a
 
-lemma periodic.mul_const_inv [division_ring α] (h : periodic f c) (a : α) :
+lemma periodic.mul_const_inv [division_semiring α] (h : periodic f c) (a : α) :
   periodic (λ x, f (x * a⁻¹)) (c * a) :=
 h.const_inv_smul₀ $ mul_opposite.op a
 
-lemma periodic.div_const [division_ring α] (h : periodic f c) (a : α) :
+lemma periodic.div_const [division_semiring α] (h : periodic f c) (a : α) :
   periodic (λ x, f (x / a)) (c * a) :=
 by simpa only [div_eq_mul_inv] using h.mul_const_inv a
 
@@ -425,12 +425,12 @@ lemma antiperiodic.const_smul [add_monoid α] [has_neg β] [group γ] [distrib_m
   antiperiodic (λ x, f (a • x)) (a⁻¹ • c) :=
 λ x, by simpa only [smul_add, smul_inv_smul] using h (a • x)
 
-lemma antiperiodic.const_smul₀ [add_comm_monoid α] [has_neg β] [division_ring γ] [module γ α]
+lemma antiperiodic.const_smul₀ [add_comm_monoid α] [has_neg β] [division_semiring γ] [module γ α]
   (h : antiperiodic f c) {a : γ} (ha : a ≠ 0) :
   antiperiodic (λ x, f (a • x)) (a⁻¹ • c) :=
 λ x, by simpa only [smul_add, smul_inv_smul₀ ha] using h (a • x)
 
-lemma antiperiodic.const_mul [division_ring α] [has_neg β]
+lemma antiperiodic.const_mul [division_semiring α] [has_neg β]
   (h : antiperiodic f c) {a : α} (ha : a ≠ 0) :
   antiperiodic (λ x, f (a * x)) (a⁻¹ * c) :=
 h.const_smul₀ ha
@@ -440,32 +440,33 @@ lemma antiperiodic.const_inv_smul [add_monoid α] [has_neg β] [group γ] [distr
   antiperiodic (λ x, f (a⁻¹ • x)) (a • c) :=
 by simpa only [inv_inv] using h.const_smul a⁻¹
 
-lemma antiperiodic.const_inv_smul₀ [add_comm_monoid α] [has_neg β] [division_ring γ] [module γ α]
+lemma antiperiodic.const_inv_smul₀
+  [add_comm_monoid α] [has_neg β] [division_semiring γ] [module γ α]
   (h : antiperiodic f c) {a : γ} (ha : a ≠ 0) :
   antiperiodic (λ x, f (a⁻¹ • x)) (a • c) :=
 by simpa only [inv_inv] using h.const_smul₀ (inv_ne_zero ha)
 
-lemma antiperiodic.const_inv_mul [division_ring α] [has_neg β]
+lemma antiperiodic.const_inv_mul [division_semiring α] [has_neg β]
   (h : antiperiodic f c) {a : α} (ha : a ≠ 0) :
   antiperiodic (λ x, f (a⁻¹ * x)) (a * c) :=
 h.const_inv_smul₀ ha
 
-lemma antiperiodic.mul_const [division_ring α] [has_neg β]
+lemma antiperiodic.mul_const [division_semiring α] [has_neg β]
   (h : antiperiodic f c) {a : α} (ha : a ≠ 0) :
   antiperiodic (λ x, f (x * a)) (c * a⁻¹) :=
 h.const_smul₀ $ (mul_opposite.op_ne_zero_iff a).mpr ha
 
-lemma antiperiodic.mul_const' [division_ring α] [has_neg β]
+lemma antiperiodic.mul_const' [division_semiring α] [has_neg β]
   (h : antiperiodic f c) {a : α} (ha : a ≠ 0) :
   antiperiodic (λ x, f (x * a)) (c / a) :=
 by simpa only [div_eq_mul_inv] using h.mul_const ha
 
-lemma antiperiodic.mul_const_inv [division_ring α] [has_neg β]
+lemma antiperiodic.mul_const_inv [division_semiring α] [has_neg β]
   (h : antiperiodic f c) {a : α} (ha : a ≠ 0) :
   antiperiodic (λ x, f (x * a⁻¹)) (c * a) :=
 h.const_inv_smul₀ $ (mul_opposite.op_ne_zero_iff a).mpr ha
 
-protected lemma antiperiodic.div_inv [division_ring α] [has_neg β]
+protected lemma antiperiodic.div_inv [division_semiring α] [has_neg β]
   (h : antiperiodic f c) {a : α} (ha : a ≠ 0) :
   antiperiodic (λ x, f (x / a)) (c * a) :=
 by simpa only [div_eq_mul_inv] using h.mul_const_inv ha
diff --git a/src/algebra/star/basic.lean b/src/algebra/star/basic.lean
@@ -310,15 +310,15 @@ lemma ring_hom.star_apply {S : Type*} [non_assoc_semiring S] [comm_semiring R] [
 alias star_ring_end_self_apply ← complex.conj_conj
 alias star_ring_end_self_apply ← is_R_or_C.conj_conj
 
-@[simp] lemma star_inv' [division_ring R] [star_ring R] (x : R) : star (x⁻¹) = (star x)⁻¹ :=
+@[simp] lemma star_inv' [division_semiring R] [star_ring R] (x : R) : star (x⁻¹) = (star x)⁻¹ :=
 op_injective $ (map_inv₀ (star_ring_equiv : R ≃+* Rᵐᵒᵖ) x).trans (op_inv (star x)).symm
 
-@[simp] lemma star_zpow₀ [division_ring R] [star_ring R] (x : R) (z : ℤ) :
+@[simp] lemma star_zpow₀ [division_semiring R] [star_ring R] (x : R) (z : ℤ) :
   star (x ^ z) = star x ^ z :=
 op_injective $ (map_zpow₀ (star_ring_equiv : R ≃+* Rᵐᵒᵖ) x z).trans (op_zpow (star x) z).symm
 
 /-- When multiplication is commutative, `star` preserves division. -/
-@[simp] lemma star_div' [field R] [star_ring R] (x y : R) : star (x / y) = star x / star y :=
+@[simp] lemma star_div' [semifield R] [star_ring R] (x y : R) : star (x / y) = star x / star y :=
 map_div₀ (star_ring_end R) _ _
 
 @[simp] lemma star_bit0 [add_monoid R] [star_add_monoid R] (r : R) :
diff --git a/src/algebra/star/module.lean b/src/algebra/star/module.lean
@@ -33,22 +33,22 @@ This file also provides some lemmas that need `algebra.module.basic` imported to
 section smul_lemmas
 variables {R M : Type*}
 
+@[simp] lemma star_nat_cast_smul [semiring R] [add_comm_monoid M] [module R M] [star_add_monoid M]
+  (n : ℕ) (x : M) : star ((n : R) • x) = (n : R) • star x :=
+map_nat_cast_smul (star_add_equiv : M ≃+ M) R R n x
+
 @[simp] lemma star_int_cast_smul [ring R] [add_comm_group M] [module R M] [star_add_monoid M]
   (n : ℤ) (x : M) : star ((n : R) • x) = (n : R) • star x :=
 map_int_cast_smul (star_add_equiv : M ≃+ M) R R n x
 
-@[simp] lemma star_nat_cast_smul [semiring R] [add_comm_monoid M] [module R M] [star_add_monoid M]
-  (n : ℕ) (x : M) : star ((n : R) • x) = (n : R) • star x :=
-map_nat_cast_smul (star_add_equiv : M ≃+ M) R R n x
+@[simp] lemma star_inv_nat_cast_smul [division_semiring R] [add_comm_monoid M] [module R M]
+  [star_add_monoid M] (n : ℕ) (x : M) : star ((n⁻¹ : R) • x) = (n⁻¹ : R) • star x :=
+map_inv_nat_cast_smul (star_add_equiv : M ≃+ M) R R n x
 
 @[simp] lemma star_inv_int_cast_smul [division_ring R] [add_comm_group M] [module R M]
   [star_add_monoid M] (n : ℤ) (x : M) : star ((n⁻¹ : R) • x) = (n⁻¹ : R) • star x :=
 map_inv_int_cast_smul (star_add_equiv : M ≃+ M) R R n x
 
-@[simp] lemma star_inv_nat_cast_smul [division_ring R] [add_comm_group M] [module R M]
-  [star_add_monoid M] (n : ℕ) (x : M) : star ((n⁻¹ : R) • x) = (n⁻¹ : R) • star x :=
-map_inv_nat_cast_smul (star_add_equiv : M ≃+ M) R R n x
-
 @[simp] lemma star_rat_cast_smul [division_ring R] [add_comm_group M] [module R M]
   [star_add_monoid M] (n : ℚ) (x : M) : star ((n : R) • x) = (n : R) • star x :=
 map_rat_cast_smul (star_add_equiv : M ≃+ M) _ _ _ x
diff --git a/src/algebra/star/pointwise.lean b/src/algebra/star/pointwise.lean
@@ -117,7 +117,7 @@ instance [has_star α] [has_trivial_star α] : has_trivial_star (set α) :=
 protected lemma star_inv [group α] [star_semigroup α] (s : set α) : (s⁻¹)⋆ = (s⋆)⁻¹ :=
 by { ext, simp only [mem_star, mem_inv, star_inv] }
 
-protected lemma star_inv' [division_ring α] [star_ring α] (s : set α) : (s⁻¹)⋆ = (s⋆)⁻¹ :=
+protected lemma star_inv' [division_semiring α] [star_ring α] (s : set α) : (s⁻¹)⋆ = (s⋆)⁻¹ :=
 by { ext, simp only [mem_star, mem_inv, star_inv'] }
 
 end set
diff --git a/src/algebra/star/self_adjoint.lean b/src/algebra/star/self_adjoint.lean
@@ -166,15 +166,20 @@ star_int_cast _
 
 end ring
 
-section division_ring
-variables [division_ring R] [star_ring R]
+section division_semiring
+variables [division_semiring R] [star_ring R]
 
 lemma inv {x : R} (hx : is_self_adjoint x) : is_self_adjoint x⁻¹ :=
 by simp only [is_self_adjoint_iff, star_inv', hx.star_eq]
 
 lemma zpow {x : R} (hx : is_self_adjoint x) (n : ℤ) : is_self_adjoint (x ^ n):=
 by simp only [is_self_adjoint_iff, star_zpow₀, hx.star_eq]
 
+end division_semiring
+
+section division_ring
+variables [division_ring R] [star_ring R]
+
 lemma _root_.is_self_adjoint_rat_cast (x : ℚ) : is_self_adjoint (x : R) :=
 star_rat_cast _
 
diff --git a/src/data/matrix/basic.lean b/src/data/matrix/basic.lean
@@ -1537,7 +1537,7 @@ matrix.ext $ by simp
   [star_add_monoid α] [module R α] (c : ℤ) (M : matrix m n α) : ((c : R) • M)ᴴ = (c : R) • Mᴴ :=
 matrix.ext $ by simp
 
-@[simp] lemma conj_transpose_inv_nat_cast_smul [division_ring R] [add_comm_group α]
+@[simp] lemma conj_transpose_inv_nat_cast_smul [division_semiring R] [add_comm_monoid α]
   [star_add_monoid α] [module R α] (c : ℕ) (M : matrix m n α) : ((c : R)⁻¹ • M)ᴴ = (c : R)⁻¹ • Mᴴ :=
 matrix.ext $ by simp
 
