feat(algebra/hom/group_instances): add missing int_cast and `nat_ca…

…st` lemmas to `add_monoid.End` and `module.End` (#15839)

We already had provided the `nat_cast` field for `add_monoid.End`, this just copies the same pattern to the three other fields, and adds the 8 missing `rfl` lemmas.



Co-authored-by: Oliver Nash <github@olivernash.org>

src/algebra/hom/group_instances.lean

@@ -69,10 +69,24 @@ instance [add_comm_monoid M] : semiring (add_monoid.End M) :=
   .. add_monoid.End.monoid M,
   .. add_monoid_hom.add_comm_monoid }
 
+/-- See also `add_monoid.End.nat_cast_def`. -/
+@[simp] lemma add_monoid.End.nat_cast_apply [add_comm_monoid M] (n : ℕ) (m : M) :
+  (↑n : add_monoid.End M) m = n • m := rfl
+
+instance [add_comm_group M] : add_comm_group (add_monoid.End M) :=
+add_monoid_hom.add_comm_group
+
 instance [add_comm_group M] : ring (add_monoid.End M) :=
-{ .. add_monoid.End.semiring,
+{ int_cast := λ z, z • 1,
+  int_cast_of_nat := of_nat_zsmul _,
+  int_cast_neg_succ_of_nat  := zsmul_neg_succ_of_nat _,
+  .. add_monoid.End.semiring,
   .. add_monoid_hom.add_comm_group }
 
+/-- See also `add_monoid.End.int_cast_def`. -/
+@[simp] lemma add_monoid.End.int_cast_apply [add_comm_group M] (z : ℤ) (m : M) :
+  (↑z : add_monoid.End M) m = z • m := rfl
+
 /-!
 ### Morphisms of morphisms
 

src/algebra/module/basic.lean

@@ -71,6 +71,9 @@ instance add_comm_monoid.nat_module : module ℕ M :=
   zero_smul := zero_nsmul,
   add_smul := λ r s x, add_nsmul x r s }
 
+lemma add_monoid.End.nat_cast_def (n : ℕ) :
+  (↑n : add_monoid.End M) = distrib_mul_action.to_add_monoid_End ℕ M n := rfl
+
 theorem add_smul : (r + s) • x = r • x + s • x := module.add_smul r s x
 
 lemma convex.combo_self {a b : R} (h : a + b = 1) (x : M) : a • x + b • x = x :=
@@ -197,6 +200,9 @@ instance add_comm_group.int_module : module ℤ M :=
   zero_smul := zero_zsmul,
   add_smul := λ r s x, add_zsmul x r s }
 
+lemma add_monoid.End.int_cast_def (z : ℤ) :
+  (↑z : add_monoid.End M) = distrib_mul_action.to_add_monoid_End ℤ M z := rfl
+
 /-- A structure containing most informations as in a module, except the fields `zero_smul`
 and `smul_zero`. As these fields can be deduced from the other ones when `M` is an `add_comm_group`,
 this provides a way to construct a module structure by checking less properties, in

src/algebra/module/linear_map.lean

@@ -811,12 +811,26 @@ instance _root_.module.End.semiring : semiring (module.End R M) :=
   zero_mul := zero_comp,
   left_distrib := λ f g h, comp_add _ _ _,
   right_distrib := λ f g h, add_comp _ _ _,
+  nat_cast := λ n, n • 1,
+  nat_cast_zero := add_monoid.nsmul_zero' _,
+  nat_cast_succ := λ n, (add_monoid.nsmul_succ' n 1).trans (add_comm _ _),
   .. add_monoid_with_one.unary,
   .. _root_.module.End.monoid,
   .. linear_map.add_comm_monoid }
 
+/-- See also `module.End.nat_cast_def`. -/
+@[simp] lemma _root_.module.End.nat_cast_apply (n : ℕ) (m : M) :
+  (↑n : module.End R M) m = n • m := rfl
+
 instance _root_.module.End.ring : ring (module.End R N₁) :=
-{ ..module.End.semiring, ..linear_map.add_comm_group }
+{ int_cast := λ z, z • 1,
+  int_cast_of_nat := of_nat_zsmul _,
+  int_cast_neg_succ_of_nat := zsmul_neg_succ_of_nat _,
+  ..module.End.semiring, ..linear_map.add_comm_group }
+
+/-- See also `module.End.int_cast_def`. -/
+@[simp] lemma _root_.module.End.int_cast_apply (z : ℤ) (m : N₁) :
+  (↑z : module.End R N₁) m = z • m := rfl
 
 section
 variables [monoid S] [distrib_mul_action S M] [smul_comm_class R S M]
@@ -930,4 +944,10 @@ def module_End_self_op : R ≃+* module.End Rᵐᵒᵖ R :=
   right_inv := λ f, linear_map.ext_ring_op $ mul_one _,
   ..module.to_module_End _ _ }
 
+lemma End.nat_cast_def (n : ℕ) [add_comm_monoid N₁] [module R N₁] :
+  (↑n : module.End R N₁) = module.to_module_End R N₁ n := rfl
+
+lemma End.int_cast_def (z : ℤ) [add_comm_group N₁] [module R N₁] :
+  (↑z : module.End R N₁) = module.to_module_End R N₁ z := rfl
+
 end module