Merge remote-tracking branch 'origin/master' into nnrat_cast

Author: YaelDillies

src/algebra/field/opposite.lean

@@ -5,6 +5,7 @@ Authors: Kenny Lau
 -/
 import algebra.field.defs
 import algebra.ring.opposite
+import data.int.cast.lemmas
 
 /-!
 # Field structure on the multiplicative/additive opposite
@@ -34,6 +35,20 @@ lemma op_rat_cast [has_rat_cast α] (q : ℚ) : op (q : α) = q := rfl
 @[simp, norm_cast, to_additive]
 lemma unop_rat_cast [has_rat_cast α] (q : ℚ) : unop (q : αᵐᵒᵖ) = q := rfl
 
+namespace mul_opposite
+
+@[to_additive] instance [has_rat_cast α] : has_rat_cast αᵐᵒᵖ := ⟨λ n, op n⟩
+
+variables {α}
+
+@[simp, norm_cast, to_additive]
+lemma op_rat_cast [has_rat_cast α] (q : ℚ) : op (q : α) = q := rfl
+
+@[simp, norm_cast, to_additive]
+lemma unop_rat_cast [has_rat_cast α] (q : ℚ) : unop (q : αᵐᵒᵖ) = q := rfl
+
+variables (α)
+
 instance [division_semiring α] : division_semiring αᵐᵒᵖ :=
 { nnrat_cast := λ q, op q,
   nnrat_cast_eq := λ q, by { rw [nnrat.cast_def, op_div, op_nat_cast, op_nat_cast, div_eq_mul_inv],
@@ -44,7 +59,7 @@ instance [division_ring α] : division_ring αᵐᵒᵖ :=
 { rat_cast := λ q, op q,
   rat_cast_mk := λ a b hb h, by { rw [rat.cast_def, op_div, op_nat_cast, op_int_cast],
     exact int.commute_cast _ _ },
-  ..mul_opposite.division_semiring, ..mul_opposite.ring α }
+  ..mul_opposite.division_semiring α, ..mul_opposite.ring α }
 
 instance [semifield α] : semifield αᵐᵒᵖ :=
 { ..mul_opposite.division_semiring, ..mul_opposite.comm_semiring α }
@@ -56,6 +71,10 @@ end mul_opposite
 
 namespace add_opposite
 
+end mul_opposite
+
+namespace add_opposite
+
 instance [division_semiring α] : division_semiring αᵃᵒᵖ :=
 { nnrat_cast := λ q, op q,
   nnrat_cast_eq := λ q, by { rw [nnrat.cast_def, op_div, op_nat_cast, op_nat_cast] },
@@ -72,6 +91,6 @@ instance [semifield α] : semifield αᵃᵒᵖ :=
 { ..add_opposite.division_semiring, ..add_opposite.comm_semiring α }
 
 instance [field α] : field αᵃᵒᵖ :=
-{ ..add_opposite.division_ring, ..add_opposite.comm_ring α }
+{ ..add_opposite.division_ring α, ..add_opposite.comm_ring α }
 
 end add_opposite

src/algebra/group/opposite.lean

@@ -24,6 +24,9 @@ namespace mul_opposite
 ### Additive structures on `αᵐᵒᵖ`
 -/
 
+@[to_additive] instance [has_nat_cast α] : has_nat_cast αᵐᵒᵖ := ⟨λ n, op n⟩
+@[to_additive] instance [has_int_cast α] : has_int_cast αᵐᵒᵖ := ⟨λ n, op n⟩
+
 instance [add_semigroup α] : add_semigroup (αᵐᵒᵖ) :=
 unop_injective.add_semigroup _ (λ x y, rfl)
 
@@ -45,9 +48,6 @@ unop_injective.add_monoid _ rfl (λ _ _, rfl) (λ _ _, rfl)
 instance [add_comm_monoid α] : add_comm_monoid αᵐᵒᵖ :=
 unop_injective.add_comm_monoid _ rfl (λ _ _, rfl) (λ _ _, rfl)
 
-@[to_additive] instance [has_nat_cast α] : has_nat_cast αᵐᵒᵖ := ⟨λ n, op n⟩
-@[to_additive] instance [has_int_cast α] : has_int_cast αᵐᵒᵖ := ⟨λ n, op n⟩
-
 instance [add_monoid_with_one α] : add_monoid_with_one αᵐᵒᵖ :=
 { nat_cast_zero := show op ((0 : ℕ) : α) = 0, by rw [nat.cast_zero, op_zero],
   nat_cast_succ := show ∀ n, op ((n + 1 : ℕ) : α) = op (n : ℕ) + 1, by simp,

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]

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

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

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

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 _
 

src/analysis/inner_product_space/adjoint.lean

@@ -434,14 +434,13 @@ open_locale complex_conjugate
 
 /-- The adjoint of the linear map associated to a matrix is the linear map associated to the
 conjugate transpose of that matrix. -/
-lemma conj_transpose_eq_adjoint (A : matrix m n 𝕜) :
-  to_lin' A.conj_transpose =
-  @linear_map.adjoint _ (euclidean_space 𝕜 n) (euclidean_space 𝕜 m) _ _ _ _ _ (to_lin' A) :=
+lemma to_euclidean_lin_conj_transpose_eq_adjoint (A : matrix m n 𝕜) :
+  A.conj_transpose.to_euclidean_lin = A.to_euclidean_lin.adjoint :=
 begin
-  rw @linear_map.eq_adjoint_iff _ (euclidean_space 𝕜 m) (euclidean_space 𝕜 n),
+  rw linear_map.eq_adjoint_iff,
   intros x y,
-  convert dot_product_assoc (conj ∘ (id x : m → 𝕜)) y A using 1,
-  simp [dot_product, mul_vec, ring_hom.map_sum,  ← star_ring_end_apply, mul_comm],
+  simp_rw [euclidean_space.inner_eq_star_dot_product, pi_Lp_equiv_to_euclidean_lin,
+    to_lin'_apply, star_mul_vec, conj_transpose_conj_transpose, dot_product_mul_vec],
 end
 
 end matrix