feat: star commutes with nnqsmul (#17351)

From LeanAPAP
leanprover-community · Oct 2, 2024 · 20a854c · 20a854c
1 parent 3c0774c
commit 20a854c
Show file tree

Hide file tree

Showing 2 changed files with 35 additions and 5 deletions.
diff --git a/Mathlib/Algebra/Star/Module.lean b/Mathlib/Algebra/Star/Module.lean
@@ -75,11 +75,43 @@ theorem star_ratCast_smul [DivisionRing R] [AddCommGroup M] [Module R M] [StarAd
 @[deprecated (since := "2024-04-17")]
 alias star_rat_cast_smul := star_ratCast_smul
 
-@[simp]
-theorem star_rat_smul {R : Type*} [AddCommGroup R] [StarAddMonoid R] [Module ℚ R] (x : R) (n : ℚ) :
-    star (n • x) = n • star x :=
+/-!
+Per the naming convention, these two lemmas call `(q • ·)` `nnrat_smul` and `rat_smul` respectively,
+rather than `nnqsmul` and `qsmul` because the latter are reserved to the actions coming from
+`DivisionSemiring` and `DivisionRing`. We provide aliases with `nnqsmul` and `qsmul` for
+discoverability.
+-/
+
+/-- Note that this lemma holds for an arbitrary `ℚ≥0`-action, rather than merely one coming from a
+`DivisionSemiring`. We keep both the `nnqsmul` and `nnrat_smul` naming conventions for
+discoverability. See `star_nnqsmul`. -/
+@[simp high]
+lemma star_nnrat_smul [AddCommMonoid R] [StarAddMonoid R] [Module ℚ≥0 R] (q : ℚ≥0) (x : R) :
+    star (q • x) = q • star x := map_nnrat_smul (starAddEquiv : R ≃+ R) _ _
+
+/-- Note that this lemma holds for an arbitrary `ℚ`-action, rather than merely one coming from a
+`DivisionRing`. We keep both the `qsmul` and `rat_smul` naming conventions for discoverability.
+See `star_qsmul`. -/
+@[simp high] lemma star_rat_smul [AddCommGroup R] [StarAddMonoid R] [Module ℚ R] (q : ℚ) (x : R) :
+    star (q • x) = q • star x :=
   map_rat_smul (starAddEquiv : R ≃+ R) _ _
 
+/-- Note that this lemma holds for an arbitrary `ℚ≥0`-action, rather than merely one coming from a
+`DivisionSemiring`. We keep both the `nnqsmul` and `nnrat_smul` naming conventions for
+discoverability. See `star_nnrat_smul`. -/
+alias star_nnqsmul := star_nnrat_smul
+
+/-- Note that this lemma holds for an arbitrary `ℚ`-action, rather than merely one coming from a
+`DivisionRing`. We keep both the `qsmul` and `rat_smul` naming conventions for
+discoverability. See `star_rat_smul`. -/
+alias star_qsmul := star_rat_smul
+
+instance StarAddMonoid.toStarModuleNNRat [AddCommMonoid R] [Module ℚ≥0 R] [StarAddMonoid R] :
+    StarModule ℚ≥0 R where star_smul := star_nnrat_smul
+
+instance StarAddMonoid.toStarModuleRat [AddCommGroup R] [Module ℚ R] [StarAddMonoid R] :
+    StarModule ℚ R where star_smul := star_rat_smul
+
 end SMulLemmas
 
 /-- If `A` is a module over a commutative `R` with compatible actions,

diff --git a/Mathlib/Data/Matrix/Basic.lean b/Mathlib/Data/Matrix/Basic.lean
@@ -2098,7 +2098,6 @@ variants which this lemma would not apply to:
 * `Matrix.conjTranspose_intCast_smul`
 * `Matrix.conjTranspose_inv_natCast_smul`
 * `Matrix.conjTranspose_inv_intCast_smul`
-* `Matrix.conjTranspose_rat_smul`
 * `Matrix.conjTranspose_ratCast_smul`
 -/
 @[simp]
@@ -2166,7 +2165,6 @@ theorem conjTranspose_ratCast_smul [DivisionRing R] [AddCommGroup α] [StarAddMo
     (c : ℚ) (M : Matrix m n α) : ((c : R) • M)ᴴ = (c : R) • Mᴴ :=
   Matrix.ext <| by simp
 
-@[simp]
 theorem conjTranspose_rat_smul [AddCommGroup α] [StarAddMonoid α] [Module ℚ α] (c : ℚ)
     (M : Matrix m n α) : (c • M)ᴴ = c • Mᴴ :=
   Matrix.ext <| by simp