feat: Every star ring is a Nat-star module (#9470)

and other basic star lemmas

From LeanAPAP

Mathlib/Algebra/Star/Basic.lean

@@ -351,10 +351,12 @@ theorem star_ratCast [DivisionRing R] [StarRing R] (r : ℚ) : star (r : R) = r
 
 end
 
+section CommSemiring
+variable [CommSemiring R] [StarRing R]
+
 /-- `star` as a ring automorphism, for commutative `R`. -/
 @[simps apply]
-def starRingAut [CommSemiring R] [StarRing R] : RingAut R :=
-  { starAddEquiv, starMulAut (R := R) with toFun := star }
+def starRingAut : RingAut R := { starAddEquiv, starMulAut (R := R) with toFun := star }
 #align star_ring_aut starRingAut
 #align star_ring_aut_apply starRingAut_apply
 
@@ -367,8 +369,7 @@ Note that this is the preferred form (over `starRingAut`, available under the sa
 because the notation `E →ₗ⋆[R] F` for an `R`-conjugate-linear map (short for
 `E →ₛₗ[starRingEnd R] F`) does not pretty-print if there is a coercion involved, as would be the
 case for `(↑starRingAut : R →* R)`. -/
-def starRingEnd [CommSemiring R] [StarRing R] : R →+* R :=
-  @starRingAut R _ _
+def starRingEnd : R →+* R := @starRingAut R _ _
 #align star_ring_end starRingEnd
 
 variable {R}
@@ -379,8 +380,7 @@ scoped[ComplexConjugate] notation "conj" => starRingEnd _
 /-- This is not a simp lemma, since we usually want simp to keep `starRingEnd` bundled.
  For example, for complex conjugation, we don't want simp to turn `conj x`
  into the bare function `star x` automatically since most lemmas are about `conj x`. -/
-theorem starRingEnd_apply [CommSemiring R] [StarRing R] {x : R} : starRingEnd R x = star x :=
-  rfl
+theorem starRingEnd_apply (x : R) : starRingEnd R x = star x := rfl
 #align star_ring_end_apply starRingEnd_apply
 
 /- Porting note: removed `simp` attribute due to report by linter:
@@ -391,28 +391,23 @@ One of the lemmas above could be a duplicate.
 If that's not the case try reordering lemmas or adding @[priority].
  -/
 -- @[simp]
-theorem starRingEnd_self_apply [CommSemiring R] [StarRing R] (x : R) :
-    starRingEnd R (starRingEnd R x) = x :=
-  star_star x
+theorem starRingEnd_self_apply (x : R) : starRingEnd R (starRingEnd R x) = x := star_star x
 #align star_ring_end_self_apply starRingEnd_self_apply
 
-instance RingHom.involutiveStar {S : Type*} [NonAssocSemiring S] [CommSemiring R] [StarRing R] :
-    InvolutiveStar (S →+* R) where
+instance RingHom.involutiveStar {S : Type*} [NonAssocSemiring S] : InvolutiveStar (S →+* R) where
   toStar := { star := fun f => RingHom.comp (starRingEnd R) f }
   star_involutive := by
     intro
     ext
     simp only [RingHom.coe_comp, Function.comp_apply, starRingEnd_self_apply]
 #align ring_hom.has_involutive_star RingHom.involutiveStar
 
-theorem RingHom.star_def {S : Type*} [NonAssocSemiring S] [CommSemiring R] [StarRing R]
-    (f : S →+* R) : Star.star f = RingHom.comp (starRingEnd R) f :=
-  rfl
+theorem RingHom.star_def {S : Type*} [NonAssocSemiring S] (f : S →+* R) :
+    Star.star f = RingHom.comp (starRingEnd R) f := rfl
 #align ring_hom.star_def RingHom.star_def
 
-theorem RingHom.star_apply {S : Type*} [NonAssocSemiring S] [CommSemiring R] [StarRing R]
-    (f : S →+* R) (s : S) : star f s = star (f s) :=
-  rfl
+theorem RingHom.star_apply {S : Type*} [NonAssocSemiring S] (f : S →+* R) (s : S) :
+    star f s = star (f s) := rfl
 #align ring_hom.star_apply RingHom.star_apply
 
 -- A more convenient name for complex conjugation
@@ -423,6 +418,12 @@ alias IsROrC.conj_conj := starRingEnd_self_apply
 set_option linter.uppercaseLean3 false in
 #align is_R_or_C.conj_conj IsROrC.conj_conj
 
+open scoped ComplexConjugate
+
+@[simp] lemma conj_trivial [TrivialStar R] (a : R) : conj a = a := star_trivial _
+
+end CommSemiring
+
 @[simp]
 theorem star_inv' [DivisionSemiring R] [StarRing R] (x : R) : star x⁻¹ = (star x)⁻¹ :=
   op_injective <| (map_inv₀ (starRingEquiv : R ≃+* Rᵐᵒᵖ) x).trans (op_inv (star x)).symm
@@ -466,6 +467,11 @@ def starRingOfComm {R : Type*} [CommSemiring R] : StarRing R :=
     star_add := fun _ _ => rfl }
 #align star_ring_of_comm starRingOfComm
 
+instance Nat.instStarRing : StarRing ℕ := starRingOfComm
+instance Rat.instStarRing : StarRing ℚ := starRingOfComm
+instance Nat.instTrivialStar : TrivialStar ℕ := ⟨fun _ ↦ rfl⟩
+instance Rat.instTrivialStar : TrivialStar ℚ := ⟨fun _ ↦ rfl⟩
+
 /-- A star module `A` over a star ring `R` is a module which is a star add monoid,
 and the two star structures are compatible in the sense
 `star (r • a) = star r • star a`.
@@ -492,6 +498,9 @@ instance StarMul.toStarModule [CommMonoid R] [StarMul R] : StarModule R R :=
   ⟨star_mul'⟩
 #align star_semigroup.to_star_module StarMul.toStarModule
 
+instance StarAddMonoid.toStarModuleNat {α} [AddCommMonoid α] [StarAddMonoid α] : StarModule ℕ α :=
+  ⟨fun n a ↦ by rw [star_nsmul, star_trivial n]⟩
+
 namespace RingHomInvPair
 
 /-- Instance needed to define star-linear maps over a commutative star ring

Mathlib/Algebra/Star/Pi.lean

@@ -61,6 +61,12 @@ theorem single_star [∀ i, AddMonoid (f i)] [∀ i, StarAddMonoid (f i)] [Decid
   single_op (fun i => @star (f i) _) (fun _ => star_zero _) i a
 #align pi.single_star Pi.single_star
 
+open scoped ComplexConjugate
+
+@[simp]
+lemma conj_apply {ι : Type*} {α : ι → Type*} [∀ i, CommSemiring (α i)] [∀ i, StarRing (α i)]
+    (f : ∀ i, α i) (i : ι) : conj f i = conj (f i) := rfl
+
 end Pi
 
 namespace Function

Mathlib/Algebra/Star/SelfAdjoint.lean

@@ -3,7 +3,7 @@ Copyright (c) 2021 Frédéric Dupuis. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Frédéric Dupuis
 -/
-import Mathlib.Algebra.Star.Basic
+import Mathlib.Algebra.Star.Pi
 import Mathlib.GroupTheory.Subgroup.Basic
 import Mathlib.Init.Data.Subtype.Basic
 
@@ -40,6 +40,7 @@ We also define `IsStarNormal R`, a `Prop` that states that an element `x` satisf
 
 -/
 
+open Function
 
 variable {R A : Type*}
 
@@ -116,8 +117,7 @@ variable [AddMonoid R] [StarAddMonoid R]
 
 variable (R)
 
-theorem _root_.isSelfAdjoint_zero : IsSelfAdjoint (0 : R) :=
-  star_zero R
+@[simp] theorem _root_.isSelfAdjoint_zero : IsSelfAdjoint (0 : R) := star_zero R
 #align is_self_adjoint_zero isSelfAdjoint_zero
 
 variable {R}
@@ -186,7 +186,7 @@ variable [MulOneClass R] [StarMul R]
 
 variable (R)
 
-theorem _root_.isSelfAdjoint_one : IsSelfAdjoint (1 : R) :=
+@[simp] theorem _root_.isSelfAdjoint_one : IsSelfAdjoint (1 : R) :=
   star_one R
 #align is_self_adjoint_one isSelfAdjoint_one
 
@@ -229,6 +229,15 @@ theorem mul {x y : R} (hx : IsSelfAdjoint x) (hy : IsSelfAdjoint y) : IsSelfAdjo
 
 end CommSemigroup
 
+section CommSemiring
+variable {α : Type*} [CommSemiring α] [StarRing α] {a : α}
+
+open scoped ComplexConjugate
+
+lemma conj_eq (ha : IsSelfAdjoint a) : conj a = a := ha.star_eq
+
+end CommSemiring
+
 section Ring
 
 variable [Ring R] [StarRing R]
@@ -593,3 +602,13 @@ instance (priority := 100) CommMonoid.isStarNormal [CommMonoid R] [StarMul R] {x
     IsStarNormal x :=
   ⟨mul_comm _ _⟩
 #align comm_monoid.is_star_normal CommMonoid.isStarNormal
+
+
+namespace Pi
+variable {ι : Type*} {α : ι → Type*} [∀ i, Star (α i)] {f : ∀ i, α i}
+
+protected lemma isSelfAdjoint : IsSelfAdjoint f ↔ ∀ i, IsSelfAdjoint (f i) := funext_iff
+
+alias ⟨_root_.IsSelfAdjoint.apply, _⟩ := Pi.isSelfAdjoint
+
+end Pi

Mathlib/Data/IsROrC/Basic.lean

@@ -932,7 +932,7 @@ theorem im_to_real {x : ℝ} : imR x = 0 :=
   rfl
 #align is_R_or_C.im_to_real IsROrC.im_to_real
 
-@[simp, isROrC_simps]
+@[isROrC_simps]
 theorem conj_to_real {x : ℝ} : conj x = x :=
   rfl
 #align is_R_or_C.conj_to_real IsROrC.conj_to_real