chore(Topology/Algebra/Module/Basic): missing cast lemmas and better …

…defeq (#8267)

Mathlib/Algebra/Module/LinearMap.lean

@@ -1093,6 +1093,11 @@ theorem _root_.Module.End.natCast_apply (n : ℕ) (m : M) : (↑n : Module.End R
   rfl
 #align module.End.nat_cast_apply Module.End.natCast_apply
 
+@[simp]
+theorem _root_.Module.End.ofNat_apply (n : ℕ) [n.AtLeastTwo] (m : M) :
+    (no_index (OfNat.ofNat n) : Module.End R M) m = OfNat.ofNat n • m :=
+  rfl
+
 instance _root_.Module.End.ring : Ring (Module.End R N₁) :=
   { Module.End.semiring, LinearMap.addCommGroup with
     intCast := fun z ↦ z • (1 : N₁ →ₗ[R] N₁)

Mathlib/Topology/Algebra/Module/Basic.lean

@@ -883,11 +883,14 @@ instance monoidWithZero : MonoidWithZero (M₁ →L[R₁] M₁) where
 theorem coe_pow (f : M₁ →L[R₁] M₁) (n : ℕ) : ⇑(f ^ n) = f^[n] :=
   hom_coe_pow _ rfl (fun _ _ ↦ rfl) _ _
 
-instance semiring [ContinuousAdd M₁] : Semiring (M₁ →L[R₁] M₁) :=
-  { ContinuousLinearMap.monoidWithZero,
-    ContinuousLinearMap.addCommMonoid with
-    left_distrib := fun f g h => ext fun x => map_add f (g x) (h x)
-    right_distrib := fun _ _ _ => ext fun _ => LinearMap.add_apply _ _ _ }
+instance semiring [ContinuousAdd M₁] : Semiring (M₁ →L[R₁] M₁) where
+  __ := ContinuousLinearMap.monoidWithZero
+  __ := ContinuousLinearMap.addCommMonoid
+  left_distrib f g h := ext fun x => map_add f (g x) (h x)
+  right_distrib _ _ _ := ext fun _ => LinearMap.add_apply _ _ _
+  natCast n := n • (1 : M₁ →L[R₁] M₁)
+  natCast_zero := zero_smul ℕ (1 : M₁ →L[R₁] M₁)
+  natCast_succ n := (AddMonoid.nsmul_succ n (1 : M₁ →L[R₁] M₁)).trans (add_comm _ _)
 #align continuous_linear_map.semiring ContinuousLinearMap.semiring
 
 /-- `ContinuousLinearMap.toLinearMap` as a `RingHom`.-/
@@ -901,6 +904,15 @@ def toLinearMapRingHom [ContinuousAdd M₁] : (M₁ →L[R₁] M₁) →+* M₁
 #align continuous_linear_map.to_linear_map_ring_hom ContinuousLinearMap.toLinearMapRingHom
 #align continuous_linear_map.to_linear_map_ring_hom_apply ContinuousLinearMap.toLinearMapRingHom_apply
 
+@[simp]
+theorem natCast_apply [ContinuousAdd M₁] (n : ℕ) (m : M₁) : (↑n : M₁ →L[R₁] M₁) m = n • m :=
+  rfl
+
+@[simp]
+theorem ofNat_apply [ContinuousAdd M₁] (n : ℕ) [n.AtLeastTwo] (m : M₁) :
+    ((no_index (OfNat.ofNat n) : M₁ →L[R₁] M₁)) m = OfNat.ofNat n • m :=
+  rfl
+
 section ApplyAction
 
 variable [ContinuousAdd M₁]
@@ -1494,11 +1506,18 @@ theorem sub_comp [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [TopologicalAddG
   simp
 #align continuous_linear_map.sub_comp ContinuousLinearMap.sub_comp
 
-instance ring [TopologicalAddGroup M] : Ring (M →L[R] M) :=
-  { ContinuousLinearMap.semiring,
-    ContinuousLinearMap.addCommGroup with }
+instance ring [TopologicalAddGroup M] : Ring (M →L[R] M) where
+  __ := ContinuousLinearMap.semiring
+  __ := ContinuousLinearMap.addCommGroup
+  intCast z := z • (1 : M →L[R] M)
+  intCast_ofNat := ofNat_zsmul _
+  intCast_negSucc := negSucc_zsmul _
 #align continuous_linear_map.ring ContinuousLinearMap.ring
 
+@[simp]
+theorem intCast_apply [TopologicalAddGroup M] (z : ℤ) (m : M) : (↑z : M →L[R] M) m = z • m :=
+  rfl
+
 theorem smulRight_one_pow [TopologicalSpace R] [TopologicalRing R] (c : R) (n : ℕ) :
     smulRight (1 : R →L[R] R) c ^ n = smulRight (1 : R →L[R] R) (c ^ n) := by
   induction' n with n ihn
@@ -1727,6 +1746,8 @@ instance algebra : Algebra R (M₂ →L[R] M₂) :=
   Algebra.ofModule smul_comp fun _ _ _ => comp_smul _ _ _
 #align continuous_linear_map.algebra ContinuousLinearMap.algebra
 
+@[simp] theorem algebraMap_apply (r : R) (m : M₂) : algebraMap R (M₂ →L[R] M₂) r m = r • m := rfl
+
 end CommRing
 
 section RestrictScalars