feat(algebra/subalgebra): missing norm_cast lemmas about operations (#…

…6790)




Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

src/algebra/algebra/subalgebra.lean

@@ -211,6 +211,30 @@ instance no_zero_smul_divisors_bot [no_zero_smul_divisors R A] : no_zero_smul_di
   from eq_zero_or_eq_zero_of_smul_eq_zero (congr_arg coe h),
   this.imp_right (@subtype.ext_iff _ _ x 0).mpr⟩
 
+@[simp, norm_cast] lemma coe_add (x y : S) : (↑(x + y) : A) = ↑x + ↑y := rfl
+@[simp, norm_cast] lemma coe_mul (x y : S) : (↑(x * y) : A) = ↑x * ↑y := rfl
+@[simp, norm_cast] lemma coe_zero : ((0 : S) : A) = 0 := rfl
+@[simp, norm_cast] lemma coe_one : ((1 : S) : A) = 1 := rfl
+@[simp, norm_cast] lemma coe_neg {R : Type u} {A : Type v} [comm_ring R] [ring A] [algebra R A]
+  {S : subalgebra R A} (x : S) : (↑(-x) : A) = -↑x := rfl
+@[simp, norm_cast] lemma coe_sub {R : Type u} {A : Type v} [comm_ring R] [ring A] [algebra R A]
+  {S : subalgebra R A} (x y : S) : (↑(x - y) : A) = ↑x - ↑y := rfl
+@[simp, norm_cast] lemma coe_smul (r : R) (x : S) : (↑(r • x) : A) = r • ↑x := rfl
+@[simp, norm_cast] lemma coe_algebra_map (r : R) : ↑(algebra_map R S r) = algebra_map R A r :=
+rfl
+
+@[simp, norm_cast] lemma coe_pow (x : S) (n : ℕ) : (↑(x^n) : A) = (↑x)^n :=
+begin
+  induction n with n ih,
+  { simp, },
+  { simp [pow_succ, ih], },
+end
+
+@[simp, norm_cast] lemma coe_eq_zero {x : S} : (x : A) = 0 ↔ x = 0 :=
+(subtype.ext_iff.symm : (x : A) = (0 : S) ↔ x = 0)
+@[simp, norm_cast] lemma coe_eq_one {x : S} : (x : A) = 1 ↔ x = 1 :=
+(subtype.ext_iff.symm : (x : A) = (1 : S) ↔ x = 1)
+
 -- todo: standardize on the names these morphisms
 -- compare with submodule.subtype
 

src/ring_theory/subsemiring.lean

@@ -159,6 +159,17 @@ instance to_semiring : semiring s :=
   left_distrib := λ x y z, subtype.eq $ left_distrib x y z,
   .. s.to_submonoid.to_monoid, .. s.to_add_submonoid.to_add_comm_monoid }
 
+@[simp, norm_cast] lemma coe_one : ((1 : s) : R) = (1 : R) := rfl
+@[simp, norm_cast] lemma coe_zero : ((0 : s) : R) = (0 : R) := rfl
+@[simp, norm_cast] lemma coe_add (x y : s) : ((x + y : s) : R) = (x + y : R) := rfl
+@[simp, norm_cast] lemma coe_mul (x y : s) : ((x * y : s) : R) = (x * y : R) := rfl
+@[simp, norm_cast] lemma coe_pow (x : s) (n : ℕ) : ((x^n : s) : R) = (x^n : R) :=
+begin
+  induction n with n ih,
+  { simp, },
+  { simp [pow_succ, ih], },
+end
+
 instance nontrivial [nontrivial R] : nontrivial s :=
 nontrivial_of_ne 0 1 $ λ H, zero_ne_one (congr_arg subtype.val H)
 
@@ -167,9 +178,6 @@ instance no_zero_divisors [no_zero_divisors R] : no_zero_divisors s :=
   or.cases_on (eq_zero_or_eq_zero_of_mul_eq_zero $ subtype.ext_iff.mp h)
     (λ h, or.inl $ subtype.eq h) (λ h, or.inr $ subtype.eq h) }
 
-@[simp, norm_cast] lemma coe_mul (x y : s) : (↑(x * y) : R) = ↑x * ↑y := rfl
-@[simp, norm_cast] lemma coe_one : ((1 : s) : R) = 1 := rfl
-
 /-- A subsemiring of a `comm_semiring` is a `comm_semiring`. -/
 instance to_comm_semiring {R} [comm_semiring R] (s : subsemiring R) : comm_semiring s :=
 { mul_comm := λ _ _, subtype.eq $ mul_comm _ _, ..s.to_semiring}