doc-next-gen

Mathlib.Algebra.Star.Basic

Module docstring

{"# Star monoids, rings, and modules

We introduce the basic algebraic notions of star monoids, star rings, and star modules. A star algebra is simply a star ring that is also a star module.

These are implemented as \"mixin\" typeclasses, so to summon a star ring (for example) one needs to write (R : Type*) [Ring R] [StarRing R]. This avoids difficulties with diamond inheritance.

For now we simply do not introduce notations, as different users are expected to feel strongly about the relative merits of r^*, r†, rᘁ, and so on.

Our star rings are actually star non-unital, non-associative, semirings, but of course we can prove star_neg : star (-r) = - star r when the underlying semiring is a ring. ","### Instances "}

Star structure
(R : Type u)
Full source 
/-- Notation typeclass (with no default notation!) for an algebraic structure with a star operation.
-/
class Star (R : Type u) where
  star : R → R
Star operation on an algebraic structure
Informal description
The structure representing an algebraic structure equipped with a star operation (involution), denoted by `* : R → R`. This operation satisfies the properties of an involution, typically including `(r*)* = r` for all `r ∈ R`. The star operation is used in various algebraic contexts such as star monoids, star rings, and star modules.
StarMemClass structure
(S R : Type*) [Star R] [SetLike S R]
Full source 
/-- `StarMemClass S G` states `S` is a type of subsets `s ⊆ G` closed under star. -/
class StarMemClass (S R : Type*) [Star R] [SetLike S R] : Prop where
  /-- Closure under star. -/
  star_mem : ∀ {s : S} {r : R}, r ∈ s → starstar r ∈ s
Star-closed subsets of a type with star operation
Informal description
The structure `StarMemClass S R` states that `S` is a type of subsets of `R` (represented via `SetLike S R`) that are closed under the star operation. That is, for any subset `s ∈ S` and any element `x ∈ s`, the star of `x` (denoted `x*`) is also in `s`.
StarMemClass.instStar instance
: Star s
Full source 
instance instStar : Star s where
  star r := ⟨star (r : R), star_mem r.prop⟩
Star Operation on Star-Closed Subsets
Informal description
For any type $S$ representing star-closed subsets of a type $R$ equipped with a star operation, the subset $s \in S$ inherits a star operation from $R$. Specifically, for any $x \in s$, the star of $x$ (denoted $x^*$) is defined as the star of $x$ in $R$ and belongs to $s$ by the star-closed property.
StarMemClass.coe_star theorem
(x : s) : star x = star (x : R)
Full source 
@[simp] lemma coe_star (x : s) : star x = star (x : R) := rfl
Star Operation Commutes with Subset Inclusion: $x^* = (x : R)^*$
Informal description
For any element $x$ in a star-closed subset $s$ of a type $R$ equipped with a star operation, the star of $x$ in $s$ is equal to the star of $x$ in $R$. That is, $x^* = (x : R)^*$.
InvolutiveStar structure
(R : Type u) extends Star R
Full source 
/-- Typeclass for a star operation with is involutive.
-/
class InvolutiveStar (R : Type u) extends Star R where
  /-- Involutive condition. -/
  star_involutive : Function.Involutive star
Involutive star operation
Informal description
The structure `InvolutiveStar` extends a type `R` equipped with a star operation (denoted by `⋆`) by requiring that the star operation is involutive, i.e., applying the star operation twice returns the original element: $\star(\star r) = r$ for all $r \in R$.
star_star theorem
[InvolutiveStar R] (r : R) : star (star r) = r
Full source 
@[simp]
theorem star_star [InvolutiveStar R] (r : R) : star (star r) = r :=
  star_involutive _
Involutivity of the Star Operation: $\star(\star r) = r$
Informal description
For any element $r$ in a type $R$ equipped with an involutive star operation $\star$, applying the star operation twice returns the original element: $\star(\star r) = r$.
star_injective theorem
[InvolutiveStar R] : Function.Injective (star : R → R)
Full source 
theorem star_injective [InvolutiveStar R] : Function.Injective (star : R → R) :=
  Function.Involutive.injective star_involutive
Injectivity of the Star Operation in Involutive Star Structures
Informal description
For any type $R$ equipped with an involutive star operation $\star$ (i.e., $\star(\star r) = r$ for all $r \in R$), the star operation $\star : R \to R$ is injective.
star_inj theorem
[InvolutiveStar R] {x y : R} : star x = star y ↔ x = y
Full source 
@[simp]
theorem star_inj [InvolutiveStar R] {x y : R} : starstar x = star y ↔ x = y :=
  star_injective.eq_iff
Injectivity of the Star Operation: $\star x = \star y \leftrightarrow x = y$
Informal description
For any elements $x$ and $y$ in a type $R$ equipped with an involutive star operation $\star$, the equality $\star x = \star y$ holds if and only if $x = y$.
Equiv.star definition
[InvolutiveStar R] : Equiv.Perm R
Full source 
/-- `star` as an equivalence when it is involutive. -/
protected def Equiv.star [InvolutiveStar R] : Equiv.Perm R :=
  star_involutive.toPerm _
Star operation as a permutation
Informal description
The function `Equiv.star` constructs a permutation (bijective map) on a type `R` equipped with an involutive star operation $\star$, where the permutation is given by the star operation itself. This means that applying the star operation twice returns the original element: $\star(\star r) = r$ for all $r \in R$.
star_eq_iff_star_eq theorem
[InvolutiveStar R] {r s : R} : star r = s ↔ star s = r
Full source 
theorem star_eq_iff_star_eq [InvolutiveStar R] {r s : R} : starstar r = s ↔ star s = r :=
  eq_comm.trans <| eq_star_iff_eq_star.trans eq_comm
Characterization of Involutive Star Operation: $\star r = s \leftrightarrow \star s = r$
Informal description
For any elements $r$ and $s$ in a type $R$ equipped with an involutive star operation $\star$, we have $\star r = s$ if and only if $\star s = r$.
TrivialStar structure
(R : Type u) [Star R]
Full source 
/-- Typeclass for a trivial star operation. This is mostly meant for `ℝ`.
-/
class TrivialStar (R : Type u) [Star R] : Prop where
  /-- Condition that star is trivial -/
  star_trivial : ∀ r : R, star r = r
Trivial star operation
Informal description
The structure representing a trivial star operation on a type \( R \), where the star operation is the identity function, i.e., \( \star r = r \) for all \( r \in R \). This is primarily used for structures like the real numbers \( \mathbb{R} \) where the star operation does not introduce any additional structure.
StarMul structure
(R : Type u) [Mul R] extends InvolutiveStar R
Full source 
/-- A `*`-magma is a magma `R` with an involutive operation `star`
such that `star (r * s) = star s * star r`.
-/
class StarMul (R : Type u) [Mul R] extends InvolutiveStar R where
  /-- `star` skew-distributes over multiplication. -/
  star_mul : ∀ r s : R, star (r * s) = star s * star r
*-magma (star-semigroup)
Informal description
A *-magma is a structure consisting of a type \( R \) equipped with a multiplication operation and an involutive operation \( \star \) (called "star") satisfying the property \( \star(r \cdot s) = \star s \cdot \star r \) for all \( r, s \in R \).
star_star_mul theorem
(x y : R) : star (star x * y) = star y * x
Full source 
theorem star_star_mul (x y : R) : star (star x * y) = star y * x := by rw [star_mul, star_star]
Star operation identity: $\star(\star x \cdot y) = \star y \cdot x$
Informal description
For any elements $x, y$ in a *-magma $R$, the star operation satisfies: \[ \star(\star x \cdot y) = \star y \cdot x. \]
star_mul_star theorem
(x y : R) : star (x * star y) = y * star x
Full source 
theorem star_mul_star (x y : R) : star (x * star y) = y * star x := by rw [star_mul, star_star]
Star operation identity: $\star(x \cdot \star y) = y \cdot \star x$
Informal description
For any elements $x, y$ in a *-magma $R$, the star operation satisfies: \[ \star(x \cdot \star y) = y \cdot \star x. \]
semiconjBy_star_star_star theorem
{x y z : R} : SemiconjBy (star x) (star z) (star y) ↔ SemiconjBy x y z
Full source 
@[simp]
theorem semiconjBy_star_star_star {x y z : R} :
    SemiconjBySemiconjBy (star x) (star z) (star y) ↔ SemiconjBy x y z := by
  simp_rw [SemiconjBy, ← star_mul, star_inj, eq_comm]
Star Semiconjugacy Equivalence: $\star x \cdot \star z = \star y \cdot \star x \leftrightarrow x \cdot y = z \cdot x$
Informal description
For any elements $x, y, z$ in a *-magma $R$, the element $\star x$ semiconjugates $\star z$ to $\star y$ if and only if $x$ semiconjugates $y$ to $z$. In other words, the following equivalence holds: \[ \star x \cdot \star z = \star y \cdot \star x \leftrightarrow x \cdot y = z \cdot x. \]
commute_star_star theorem
{x y : R} : Commute (star x) (star y) ↔ Commute x y
Full source 
@[simp]
theorem commute_star_star {x y : R} : CommuteCommute (star x) (star y) ↔ Commute x y :=
  semiconjBy_star_star_star
Star Commutation Equivalence: $\star x \star y = \star y \star x \leftrightarrow xy = yx$
Informal description
For any elements $x, y$ in a *-magma $R$, the elements $\star x$ and $\star y$ commute if and only if $x$ and $y$ commute. In other words: \[ \star x \cdot \star y = \star y \cdot \star x \leftrightarrow x \cdot y = y \cdot x. \]
commute_star_comm theorem
{x y : R} : Commute (star x) y ↔ Commute x (star y)
Full source 
theorem commute_star_comm {x y : R} : CommuteCommute (star x) y ↔ Commute x (star y) := by
  rw [← commute_star_star, star_star]
Star Commutation Equivalence: $\star x$ commutes with $y$ $\leftrightarrow$ $x$ commutes with $\star y$
Informal description
For any elements $x, y$ in a *-magma $R$, the element $\star x$ commutes with $y$ if and only if $x$ commutes with $\star y$. In other words: \[ \star x \cdot y = y \cdot \star x \leftrightarrow x \cdot \star y = \star y \cdot x. \]
star_mul' theorem
[CommMagma R] [StarMul R] (x y : R) : star (x * y) = star x * star y
Full source 
/-- In a commutative ring, make `simp` prefer leaving the order unchanged. -/
@[simp]
theorem star_mul' [CommMagma R] [StarMul R] (x y : R) : star (x * y) = star x * star y :=
  (star_mul x y).trans (mul_comm _ _)
Star Operation Preserves Multiplication in Commutative Magmas
Informal description
In a commutative magma $R$ equipped with a star operation, the star of the product of two elements $x$ and $y$ equals the product of their stars, i.e., \[ \star(x \cdot y) = \star x \cdot \star y. \]
starMulEquiv definition
[Mul R] [StarMul R] : R ≃* Rᵐᵒᵖ
Full source 
/-- `star` as a `MulEquiv` from `R` to `Rᵐᵒᵖ` -/
@[simps apply]
def starMulEquiv [Mul R] [StarMul R] : R ≃* Rᵐᵒᵖ :=
  { (InvolutiveStar.star_involutive.toPerm star).trans opEquiv with
    toFun := fun x => MulOpposite.op (star x)
    map_mul' := fun x y => by simp only [star_mul, op_mul] }
Star operation as a multiplicative equivalence to the opposite
Informal description
The multiplicative equivalence `starMulEquiv` maps an element \( x \) of a type \( R \) with multiplication and a star operation to its star \( \star x \) in the multiplicative opposite \( R^\text{op} \). This equivalence satisfies the property that for any \( x, y \in R \), the star of the product \( x \cdot y \) is mapped to the product \( \star y \cdot \star x \) in \( R^\text{op} \).
starMulAut definition
[CommSemigroup R] [StarMul R] : MulAut R
Full source 
/-- `star` as a `MulAut` for commutative `R`. -/
@[simps apply]
def starMulAut [CommSemigroup R] [StarMul R] : MulAut R :=
  { InvolutiveStar.star_involutive.toPerm star with
    toFun := star
    map_mul' := star_mul' }
Star operation as a multiplicative automorphism on a commutative semigroup
Informal description
For a commutative semigroup \( R \) equipped with a star operation satisfying the *-magma property, the function `starMulAut` constructs a multiplicative automorphism of \( R \). This automorphism is given by the star operation, which is involutive (i.e., \(\text{star}(\text{star}(x)) = x\) for all \(x \in R\)) and satisfies \(\text{star}(x \cdot y) = \text{star}(x) \cdot \text{star}(y)\) for all \(x, y \in R\).
star_one theorem
[MulOneClass R] [StarMul R] : star (1 : R) = 1
Full source 
@[simp]
theorem star_one [MulOneClass R] [StarMul R] : star (1 : R) = 1 :=
  op_injective <| (starMulEquiv : R ≃* Rᵐᵒᵖ).map_one.trans op_one.symm
Star operation preserves the multiplicative identity: $\star(1) = 1$
Informal description
For any type $R$ equipped with a multiplication operation and a multiplicative identity element (i.e., a `MulOneClass` structure) and an involutive star operation satisfying the *-magma property, the star of the identity element $1 \in R$ is equal to $1$ itself, i.e., $\star(1) = 1$.
star_pow theorem
[Monoid R] [StarMul R] (x : R) (n : ℕ) : star (x ^ n) = star x ^ n
Full source 
@[simp]
theorem star_pow [Monoid R] [StarMul R] (x : R) (n : ℕ) : star (x ^ n) = star x ^ n :=
  op_injective <|
    ((starMulEquiv : R ≃* Rᵐᵒᵖ).toMonoidHom.map_pow x n).trans (op_pow (star x) n).symm
Star operation commutes with powers: $\star(x^n) = (\star x)^n$
Informal description
Let $R$ be a monoid equipped with a star operation $\star$ satisfying the property $\star(r \cdot s) = \star s \cdot \star r$ for all $r, s \in R$. Then for any element $x \in R$ and any natural number $n$, the star of the $n$-th power of $x$ equals the $n$-th power of the star of $x$, i.e., $\star(x^n) = (\star x)^n$.
star_inv theorem
[Group R] [StarMul R] (x : R) : star x⁻¹ = (star x)⁻¹
Full source 
@[simp]
theorem star_inv [Group R] [StarMul R] (x : R) : star x⁻¹ = (star x)⁻¹ :=
  op_injective <| ((starMulEquiv : R ≃* Rᵐᵒᵖ).toMonoidHom.map_inv x).trans (op_inv (star x)).symm
Star Preserves Inversion in Groups: $\star(x^{-1}) = (\star x)^{-1}$
Informal description
Let $R$ be a group equipped with a star operation satisfying the *-magma property. Then for any element $x \in R$, the star operation preserves inversion, i.e., \[ \star(x^{-1}) = (\star x)^{-1}. \]
star_zpow theorem
[Group R] [StarMul R] (x : R) (z : ℤ) : star (x ^ z) = star x ^ z
Full source 
@[simp]
theorem star_zpow [Group R] [StarMul R] (x : R) (z : ℤ) : star (x ^ z) = star x ^ z :=
  op_injective <|
    ((starMulEquiv : R ≃* Rᵐᵒᵖ).toMonoidHom.map_zpow x z).trans (op_zpow (star x) z).symm
Star Operation Preserves Integer Powers: $\star(x^z) = (\star x)^z$
Informal description
Let $R$ be a group equipped with a star operation satisfying the *-magma property. Then for any element $x \in R$ and any integer $z$, the star operation preserves integer powers, i.e., \[ \star(x^z) = (\star x)^z. \]
star_div theorem
[CommGroup R] [StarMul R] (x y : R) : star (x / y) = star x / star y
Full source 
/-- When multiplication is commutative, `star` preserves division. -/
@[simp]
theorem star_div [CommGroup R] [StarMul R] (x y : R) : star (x / y) = star x / star y :=
  map_div (starMulAut : R ≃* R) _ _
Star Preserves Division in Commutative Groups: $\star(x / y) = \star x / \star y$
Informal description
Let $R$ be a commutative group equipped with a star operation satisfying the *-magma property. Then for any elements $x, y \in R$, the star operation preserves division, i.e., \[ \star\left(\frac{x}{y}\right) = \frac{\star x}{\star y}. \]
starMulOfComm abbrev
{R : Type*} [CommMonoid R] : StarMul R
Full source 
/-- Any commutative monoid admits the trivial `*`-structure.

See note [reducible non-instances].
-/
abbrev starMulOfComm {R : Type*} [CommMonoid R] : StarMul R where
  star := id
  star_involutive _ := rfl
  star_mul := mul_comm
Trivial Star-Multiplicative Structure on Commutative Monoids
Informal description
For any commutative monoid $R$, there exists a trivial star-multiplicative structure on $R$ where the star operation is the identity function, i.e., $\star r = r$ for all $r \in R$.
star_id_of_comm theorem
{R : Type*} [CommMonoid R] {x : R} : star x = x
Full source 
/-- Note that since `starMulOfComm` is reducible, `simp` can already prove this. -/
theorem star_id_of_comm {R : Type*} [CommMonoid R] {x : R} : star x = x :=
  rfl
Star Operation is Identity on Commutative Monoids
Informal description
For any commutative monoid $R$ and any element $x \in R$, the star operation acts as the identity function, i.e., $\star x = x$.
StarAddMonoid structure
(R : Type u) [AddMonoid R] extends InvolutiveStar R
Full source 
/-- A `*`-additive monoid `R` is an additive monoid with an involutive `star` operation which
preserves addition. -/
class StarAddMonoid (R : Type u) [AddMonoid R] extends InvolutiveStar R where
  /-- `star` commutes with addition -/
  star_add : ∀ r s : R, star (r + s) = star r + star s
Star Additive Monoid
Informal description
A *-additive monoid is an additive monoid \( R \) equipped with an involutive star operation \( \star \) that preserves addition, i.e., \( \star (a + b) = \star a + \star b \) for all \( a, b \in R \).
starAddEquiv definition
[AddMonoid R] [StarAddMonoid R] : R ≃+ R
Full source 
/-- `star` as an `AddEquiv` -/
@[simps apply]
def starAddEquiv [AddMonoid R] [StarAddMonoid R] : R ≃+ R :=
  { InvolutiveStar.star_involutive.toPerm star with
    toFun := star
    map_add' := star_add }
Star operation as an additive equivalence
Informal description
The function `starAddEquiv` is an additive equivalence (additive isomorphism) on a type `R` equipped with an additive monoid structure and a star operation that is involutive and preserves addition. Specifically, it maps each element $x \in R$ to its star $\star x$, and satisfies $\star(a + b) = \star a + \star b$ for all $a, b \in R$.
star_zero theorem
[AddMonoid R] [StarAddMonoid R] : star (0 : R) = 0
Full source 
@[simp]
theorem star_zero [AddMonoid R] [StarAddMonoid R] : star (0 : R) = 0 :=
  (starAddEquiv : R ≃+ R).map_zero
Star of Zero Equals Zero in Star Additive Monoids
Informal description
For any additive monoid $R$ equipped with a star operation, the star of the zero element is equal to zero, i.e., $\star(0) = 0$.
star_eq_zero theorem
[AddMonoid R] [StarAddMonoid R] {x : R} : star x = 0 ↔ x = 0
Full source 
@[simp]
theorem star_eq_zero [AddMonoid R] [StarAddMonoid R] {x : R} : starstar x = 0 ↔ x = 0 :=
  starAddEquiv.map_eq_zero_iff (M := R)
Star of Zero Equivalence in Additive Monoids
Informal description
For any element $x$ in an additive monoid $R$ equipped with a star operation, the star of $x$ is equal to zero if and only if $x$ itself is equal to zero, i.e., $\star x = 0 \leftrightarrow x = 0$.
star_ne_zero theorem
[AddMonoid R] [StarAddMonoid R] {x : R} : star x ≠ 0 ↔ x ≠ 0
Full source 
theorem star_ne_zero [AddMonoid R] [StarAddMonoid R] {x : R} : starstar x ≠ 0star x ≠ 0 ↔ x ≠ 0 := by
  simp only [ne_eq, star_eq_zero]
Nonzero Preservation under Star Operation in Additive Monoids
Informal description
For any element $x$ in an additive monoid $R$ equipped with a star operation, the star of $x$ is nonzero if and only if $x$ itself is nonzero, i.e., $\star x \neq 0 \leftrightarrow x \neq 0$.
star_neg theorem
[AddGroup R] [StarAddMonoid R] (r : R) : star (-r) = -star r
Full source 
@[simp]
theorem star_neg [AddGroup R] [StarAddMonoid R] (r : R) : star (-r) = -star r :=
  (starAddEquiv : R ≃+ R).map_neg _
Star Operation Commutes with Negation in Additive Groups
Informal description
For any element $r$ in an additive group $R$ equipped with a star operation that is an additive monoid homomorphism, the star of the negation of $r$ is equal to the negation of the star of $r$, i.e., $\star(-r) = -\star r$.
star_sub theorem
[AddGroup R] [StarAddMonoid R] (r s : R) : star (r - s) = star r - star s
Full source 
@[simp]
theorem star_sub [AddGroup R] [StarAddMonoid R] (r s : R) : star (r - s) = star r - star s :=
  (starAddEquiv : R ≃+ R).map_sub _ _
Star Operation Preserves Subtraction in Additive Groups
Informal description
Let $R$ be an additive group equipped with a star operation that is an additive monoid homomorphism. For any elements $r, s \in R$, the star of the difference $r - s$ equals the difference of the stars, i.e., $\star(r - s) = \star r - \star s$.
star_nsmul theorem
[AddMonoid R] [StarAddMonoid R] (n : ℕ) (x : R) : star (n • x) = n • star x
Full source 
@[simp]
theorem star_nsmul [AddMonoid R] [StarAddMonoid R] (n : ℕ) (x : R) : star (n • x) = n • star x :=
  (starAddEquiv : R ≃+ R).toAddMonoidHom.map_nsmul _ _
Star Operation Commutes with Natural Scalar Multiplication
Informal description
For any additive monoid $R$ equipped with a star operation that is involutive and additive, and for any natural number $n$ and element $x \in R$, the star of the $n$-fold scalar multiplication of $x$ equals the $n$-fold scalar multiplication of the star of $x$, i.e., $\star(n \cdot x) = n \cdot \star x$.
star_zsmul theorem
[AddGroup R] [StarAddMonoid R] (n : ℤ) (x : R) : star (n • x) = n • star x
Full source 
@[simp]
theorem star_zsmul [AddGroup R] [StarAddMonoid R] (n : ℤ) (x : R) : star (n • x) = n • star x :=
  (starAddEquiv : R ≃+ R).toAddMonoidHom.map_zsmul _ _
Star Operation Commutes with Integer Scalar Multiplication
Informal description
Let $R$ be an additive group equipped with a star operation that is involutive and additive. For any integer $n$ and any element $x \in R$, the star of the integer scalar multiple $n \cdot x$ is equal to the integer scalar multiple of the star of $x$, i.e., $\star(n \cdot x) = n \cdot \star x$.
StarRing structure
(R : Type u) [NonUnitalNonAssocSemiring R] extends StarMul R
Full source 
/-- A `*`-ring `R` is a non-unital, non-associative (semi)ring with an involutive `star` operation
which is additive which makes `R` with its multiplicative structure into a `*`-multiplication
(i.e. `star (r * s) = star s * star r`). -/
class StarRing (R : Type u) [NonUnitalNonAssocSemiring R] extends StarMul R where
  /-- `star` commutes with addition -/
  star_add : ∀ r s : R, star (r + s) = star r + star s
*-ring
Informal description
A *-ring \( R \) is a non-unital, non-associative (semi)ring equipped with an involutive star operation \( \star \) that is additive and satisfies the property \( \star(r \cdot s) = \star s \cdot \star r \) for all \( r, s \in R \). This makes \( R \) into a *-multiplication structure.
StarRing.toStarAddMonoid instance
[NonUnitalNonAssocSemiring R] [StarRing R] : StarAddMonoid R
Full source 
instance (priority := 100) StarRing.toStarAddMonoid [NonUnitalNonAssocSemiring R] [StarRing R] :
    StarAddMonoid R where
  star_add := StarRing.star_add
*-rings are *-additive monoids
Informal description
Every *-ring \( R \) is also a *-additive monoid. That is, if \( R \) is a non-unital, non-associative semiring equipped with an involutive star operation that is additive and satisfies \( \star(r \cdot s) = \star s \cdot \star r \) for all \( r, s \in R \), then \( R \) inherits the structure of a *-additive monoid where the star operation preserves addition.
starRingEquiv definition
[NonUnitalNonAssocSemiring R] [StarRing R] : R ≃+* Rᵐᵒᵖ
Full source 
/-- `star` as a `RingEquiv` from `R` to `Rᵐᵒᵖ` -/
@[simps apply]
def starRingEquiv [NonUnitalNonAssocSemiring R] [StarRing R] : R ≃+* Rᵐᵒᵖ :=
  { starAddEquiv.trans (MulOpposite.opAddEquiv : R ≃+ Rᵐᵒᵖ), starMulEquiv with
    toFun := fun x => MulOpposite.op (star x) }
Star operation as a ring equivalence to the opposite
Informal description
The function `starRingEquiv` is a ring equivalence (ring isomorphism) between a non-unital, non-associative semiring \( R \) equipped with a star ring structure and its multiplicative opposite \( R^\text{op} \). It maps each element \( x \in R \) to the opposite of its star \( \text{op}(\star x) \), combining the additive and multiplicative properties of the star operation. Specifically, it satisfies: - Additivity: \( \text{op}(\star(x + y)) = \text{op}(\star x) + \text{op}(\star y) \), - Multiplicativity: \( \text{op}(\star(x \cdot y)) = \text{op}(\star y) \cdot \text{op}(\star x) \).
star_natCast theorem
[NonAssocSemiring R] [StarRing R] (n : ℕ) : star (n : R) = n
Full source 
@[simp, norm_cast]
theorem star_natCast [NonAssocSemiring R] [StarRing R] (n : ℕ) : star (n : R) = n :=
  (congr_arg unop (map_natCast (starRingEquiv : R ≃+* Rᵐᵒᵖ) n)).trans (unop_natCast _)
Star Operation Fixes Natural Number Scalars: $\star(n) = n$
Informal description
For any natural number $n$ in a non-associative semiring $R$ equipped with a star ring structure, the star operation applied to $n$ is equal to $n$ itself, i.e., $\star(n) = n$.
star_ofNat theorem
[NonAssocSemiring R] [StarRing R] (n : ℕ) [n.AtLeastTwo] : star (ofNat(n) : R) = ofNat(n)
Full source 
@[simp]
theorem star_ofNat [NonAssocSemiring R] [StarRing R] (n : ℕ) [n.AtLeastTwo] :
    star (ofNat(n) : R) = ofNat(n) :=
  star_natCast _
Star Operation Fixes Numerals ≥ 2: $\star(n) = n$
Informal description
For any natural number $n \geq 2$ in a non-associative semiring $R$ equipped with a star ring structure, the star operation applied to the canonical image of $n$ in $R$ is equal to the canonical image of $n$ itself, i.e., $\star(n) = n$.
star_intCast theorem
[NonAssocRing R] [StarRing R] (z : ℤ) : star (z : R) = z
Full source 
@[simp, norm_cast]
theorem star_intCast [NonAssocRing R] [StarRing R] (z : ℤ) : star (z : R) = z :=
  (congr_arg unop <| map_intCast (starRingEquiv : R ≃+* Rᵐᵒᵖ) z).trans (unop_intCast _)
Star Operation Fixes Integer Scalars: $\star(z) = z$
Informal description
For any integer $z$ in a non-associative ring $R$ equipped with a star ring structure, the star operation applied to $z$ is equal to $z$ itself, i.e., $\star(z) = z$.
starRingAut definition
: RingAut R
Full source 
/-- `star` as a ring automorphism, for commutative `R`. -/
@[simps apply]
def starRingAut : RingAut R := { starAddEquiv, starMulAut (R := R) with toFun := star }
Star ring automorphism
Informal description
The function `starRingAut` is a ring automorphism (i.e., a bijective ring homomorphism from \( R \) to itself) defined by the star operation on a commutative ring \( R \). It satisfies the properties: 1. \(\text{starRingAut}(x + y) = \text{starRingAut}(x) + \text{starRingAut}(y)\) 2. \(\text{starRingAut}(x \cdot y) = \text{starRingAut}(x) \cdot \text{starRingAut}(y)\) 3. \(\text{starRingAut}(1) = 1\) 4. \(\text{starRingAut}(\text{starRingAut}(x)) = x\) (involutivity)
starRingEnd definition
: R →+* R
Full source 
/-- `star` as a ring endomorphism, for commutative `R`. This is used to denote complex
conjugation, and is available under the notation `conj` in the locale `ComplexConjugate`.

Note that this is the preferred form (over `starRingAut`, available under the same hypotheses)
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 : R →+* R := @starRingAut R _ _
Star ring endomorphism
Informal description
The function `starRingEnd` is a ring endomorphism (i.e., a ring homomorphism from $R$ to itself) defined by the star operation on a commutative ring $R$. It satisfies the properties: 1. $\text{starRingEnd}(x + y) = \text{starRingEnd}(x) + \text{starRingEnd}(y)$ 2. $\text{starRingEnd}(x \cdot y) = \text{starRingEnd}(x) \cdot \text{starRingEnd}(y)$ 3. $\text{starRingEnd}(1) = 1$
starRingEnd_apply theorem
(x : R) : starRingEnd R x = star x
Full source 
/-- 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 (x : R) : starRingEnd R x = star x := rfl
Star Ring Endomorphism Evaluation: $\text{starRingEnd}(x) = \star x$
Informal description
For any element $x$ in a *-ring $R$, the evaluation of the star ring endomorphism at $x$ equals the star operation applied to $x$, i.e., $\text{starRingEnd}(x) = \star x$.
starRingEnd_self_apply theorem
(x : R) : starRingEnd R (starRingEnd R x) = x
Full source 
theorem starRingEnd_self_apply (x : R) : starRingEnd R (starRingEnd R x) = x := star_star x
Involutivity of the Star Ring Endomorphism: $\text{starRingEnd}_R \circ \text{starRingEnd}_R = \text{id}$
Informal description
For any element $x$ in a commutative ring $R$ equipped with an involutive star operation $\star$, applying the star ring endomorphism twice returns the original element, i.e., $\text{starRingEnd}_R(\text{starRingEnd}_R(x)) = x$.
RingHom.involutiveStar instance
{S : Type*} [NonAssocSemiring S] : InvolutiveStar (S →+* R)
Full source 
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]
Involutive Star Structure on Ring Homomorphisms
Informal description
For any non-associative semiring $S$ and ring homomorphisms $f : S \to R$ where $R$ is equipped with an involutive star operation, the set of ring homomorphisms $S \to R$ forms an involutive star structure where the star operation is defined by $(\star f)(x) = \star(f(x))$ for all $x \in S$.
RingHom.star_def theorem
{S : Type*} [NonAssocSemiring S] (f : S →+* R) : Star.star f = RingHom.comp (starRingEnd R) f
Full source 
theorem RingHom.star_def {S : Type*} [NonAssocSemiring S] (f : S →+* R) :
    Star.star f = RingHom.comp (starRingEnd R) f := rfl
Definition of Star Operation on Ring Homomorphisms via Composition
Informal description
For any non-associative semiring $S$ and ring homomorphism $f \colon S \to R$, the star operation on $f$ is given by the composition of $f$ with the star ring endomorphism of $R$, i.e., $\star f = \text{starRingEnd}_R \circ f$.
RingHom.star_apply theorem
{S : Type*} [NonAssocSemiring S] (f : S →+* R) (s : S) : star f s = star (f s)
Full source 
theorem RingHom.star_apply {S : Type*} [NonAssocSemiring S] (f : S →+* R) (s : S) :
    star f s = star (f s) := rfl
Star Operation on Ring Homomorphisms Evaluates Pointwise
Informal description
For any non-associative semiring $S$ and ring homomorphism $f \colon S \to R$ (where $R$ is equipped with an involutive star operation), the star operation applied to $f$ evaluated at $s \in S$ equals the star operation applied to $f(s)$. That is, $(\star f)(s) = \star(f(s))$.
conj_trivial theorem
[TrivialStar R] (a : R) : conj a = a
Full source 
@[simp] lemma conj_trivial [TrivialStar R] (a : R) : conj a = a := star_trivial _
Conjugate Equals Identity under Trivial Star Operation
Informal description
For any element $a$ in a ring $R$ equipped with the trivial star operation (where $\star r = r$ for all $r \in R$), the conjugate of $a$ is equal to $a$ itself, i.e., $\text{conj}(a) = a$.
star_inv₀ theorem
[GroupWithZero R] [StarMul R] (x : R) : star x⁻¹ = (star x)⁻¹
Full source 
@[simp]
theorem star_inv₀ [GroupWithZero R] [StarMul R] (x : R) : star x⁻¹ = (star x)⁻¹ :=
  op_injective <| (map_inv₀ (starMulEquiv : R ≃* Rᵐᵒᵖ) x).trans (op_inv (star x)).symm
Star Operation Commutes with Inversion in Groups with Zero: $\star(x^{-1}) = (\star x)^{-1}$
Informal description
For any element $x$ in a group with zero $R$ equipped with a star multiplication operation, the star of the inverse of $x$ is equal to the inverse of the star of $x$, i.e., $\star(x^{-1}) = (\star x)^{-1}$.
star_zpow₀ theorem
[GroupWithZero R] [StarMul R] (x : R) (z : ℤ) : star (x ^ z) = star x ^ z
Full source 
@[simp]
theorem star_zpow₀ [GroupWithZero R] [StarMul R] (x : R) (z : ℤ) : star (x ^ z) = star x ^ z :=
  op_injective <| (map_zpow₀ (starMulEquiv : R ≃* Rᵐᵒᵖ) x z).trans (op_zpow (star x) z).symm
Star Operation Commutes with Integer Powers in Groups with Zero: $\star(x^z) = (\star x)^z$
Informal description
Let $R$ be a group with zero equipped with a star operation $\star$ that is multiplicative (i.e., $\star(r \cdot s) = \star s \cdot \star r$ for all $r, s \in R$). Then for any element $x \in R$ and any integer $z$, the star of $x^z$ equals the $z$-th power of the star of $x$, i.e., $\star(x^z) = (\star x)^z$.
star_div₀ theorem
[CommGroupWithZero R] [StarMul R] (x y : R) : star (x / y) = star x / star y
Full source 
/-- When multiplication is commutative, `star` preserves division. -/
@[simp]
theorem star_div₀ [CommGroupWithZero R] [StarMul R] (x y : R) : star (x / y) = star x / star y := by
  apply op_injective
  rw [division_def, op_div, mul_comm, star_mul, star_inv₀, op_mul, op_inv]
Star Operation Preserves Division in Commutative Groups with Zero: $\star(x / y) = \star x / \star y$
Informal description
Let $R$ be a commutative group with zero equipped with a star operation $\star$ that is multiplicative (i.e., $\star(r \cdot s) = \star s \cdot \star r$ for all $r, s \in R$). Then for any elements $x, y \in R$, the star of the quotient $x / y$ equals the quotient of the stars, i.e., $\star(x / y) = \star x / \star y$.
starRingOfComm abbrev
{R : Type*} [CommSemiring R] : StarRing R
Full source 
/-- Any commutative semiring admits the trivial `*`-structure.

See note [reducible non-instances].
-/
abbrev starRingOfComm {R : Type*} [CommSemiring R] : StarRing R :=
  { starMulOfComm with
    star_add := fun _ _ => rfl }
Trivial Star-Ring Structure on Commutative Semirings
Informal description
For any commutative semiring $R$, there exists a trivial $*$-ring structure on $R$ where the star operation is the identity function, i.e., $\star r = r$ for all $r \in R$.
Nat.instStarRing instance
: StarRing ℕ
Full source 
instance Nat.instStarRing : StarRing ℕ := starRingOfComm
Natural Numbers as a Trivial *-Ring
Informal description
The natural numbers $\mathbb{N}$ form a *-ring with the trivial star operation, where $\star n = n$ for all $n \in \mathbb{N}$.
Int.instStarRing instance
: StarRing ℤ
Full source 
instance Int.instStarRing : StarRing ℤ := starRingOfComm
The Trivial *-Ring Structure on Integers
Informal description
The integers $\mathbb{Z}$ form a *-ring with the trivial star operation, where $\star r = r$ for all $r \in \mathbb{Z}$.
Nat.instTrivialStar instance
: TrivialStar ℕ
Full source 
instance Nat.instTrivialStar : TrivialStar ℕ := ⟨fun _ ↦ rfl⟩
Trivial Star Operation on Natural Numbers
Informal description
The natural numbers $\mathbb{N}$ are equipped with the trivial star operation, where $\star n = n$ for all $n \in \mathbb{N}$.
Int.instTrivialStar instance
: TrivialStar ℤ
Full source 
instance Int.instTrivialStar : TrivialStar ℤ := ⟨fun _ ↦ rfl⟩
Trivial Star Operation on Integers
Informal description
The integers $\mathbb{Z}$ are equipped with the trivial star operation, where $\star r = r$ for all $r \in \mathbb{Z}$.
StarModule structure
(R : Type u) (A : Type v) [Star R] [Star A] [SMul R A]
Full source 
/-- 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`.

Note that it is up to the user of this typeclass to enforce
`[Semiring R] [StarRing R] [AddCommMonoid A] [StarAddMonoid A] [Module R A]`, and that
the statement only requires `[Star R] [Star A] [SMul R A]`.

If used as `[CommRing R] [StarRing R] [Semiring A] [StarRing A] [Algebra R A]`, this represents a
star algebra.
-/

class StarModule (R : Type u) (A : Type v) [Star R] [Star A] [SMul R A] : Prop where
  /-- `star` commutes with scalar multiplication -/
  star_smul : ∀ (r : R) (a : A), star (r • a) = star r • star a
Star Module
Informal description
A star module $A$ over a star ring $R$ is a module equipped with a star operation (involution) that is compatible with the scalar multiplication, satisfying the condition $\star(r \cdot a) = \star r \cdot \star a$ for all $r \in R$ and $a \in A$. This structure requires $R$ to be a star ring and $A$ to be a star additive monoid, with the module action of $R$ on $A$ respecting the star operations.
StarMul.toStarModule instance
[CommMonoid R] [StarMul R] : StarModule R R
Full source 
/-- A commutative star monoid is a star module over itself via `Monoid.toMulAction`. -/
instance StarMul.toStarModule [CommMonoid R] [StarMul R] : StarModule R R :=
  ⟨star_mul'⟩
Commutative Star Monoid as a Star Module over Itself
Informal description
For any commutative monoid $R$ equipped with a star operation that preserves multiplication (i.e., $\star(x \cdot y) = \star x \cdot \star y$ for all $x, y \in R$), $R$ is a star module over itself under the left multiplication action.
StarAddMonoid.toStarModuleNat instance
{α} [AddCommMonoid α] [StarAddMonoid α] : StarModule ℕ α
Full source 
instance StarAddMonoid.toStarModuleNat {α} [AddCommMonoid α] [StarAddMonoid α] :
    StarModule ℕ α where star_smul := star_nsmul
Natural Number Star Module Structure on Star Additive Monoids
Informal description
For any additive commutative monoid $\alpha$ equipped with a star operation that is involutive and additive, $\alpha$ is a star module over the natural numbers $\mathbb{N}$ with the trivial star operation. This means that for any natural number $n$ and element $x \in \alpha$, the star operation commutes with scalar multiplication: $\star(n \cdot x) = n \cdot \star x$.
StarAddMonoid.toStarModuleInt instance
{α} [AddCommGroup α] [StarAddMonoid α] : StarModule ℤ α
Full source 
instance StarAddMonoid.toStarModuleInt {α} [AddCommGroup α] [StarAddMonoid α] : StarModule ℤ α where
  star_smul := star_zsmul
Integer Star Module Structure on Star Additive Groups
Informal description
For any additive commutative group $\alpha$ equipped with a star operation that is involutive and additive, $\alpha$ is a star module over the integers $\mathbb{Z}$ with the trivial star operation. This means that for any integer $n$ and element $x \in \alpha$, the star operation commutes with scalar multiplication: $\star(n \cdot x) = n \cdot \star x$.
RingHomInvPair.instStarRingEnd instance
[CommSemiring R] [StarRing R] : RingHomInvPair (starRingEnd R) (starRingEnd R)
Full source 
/-- Instance needed to define star-linear maps over a commutative star ring
(ex: conjugate-linear maps when R = ℂ). -/
instance [CommSemiring R] [StarRing R] : RingHomInvPair (starRingEnd R) (starRingEnd R) :=
  ⟨RingHom.ext star_star, RingHom.ext star_star⟩
Star Ring Endomorphism as an Involutive Ring Automorphism
Informal description
For any commutative semiring $R$ equipped with a star ring structure, the star ring endomorphism $\text{starRingEnd}$ on $R$ forms a ring homomorphism inverse pair with itself. That is, $\text{starRingEnd}$ is an involutive ring automorphism of $R$.
StarHomClass structure
(F : Type*) (R S : outParam Type*) [Star R] [Star S] [FunLike F R S]
Full source 
/-- `StarHomClass F R S` states that `F` is a type of `star`-preserving maps from `R` to `S`. -/
class StarHomClass (F : Type*) (R S : outParam Type*) [Star R] [Star S] [FunLike F R S] : Prop where
  /-- the maps preserve star -/
  map_star : ∀ (f : F) (r : R), f (star r) = star (f r)
Star-Preserving Homomorphism Class
Informal description
The class `StarHomClass F R S` asserts that `F` is a type of maps from `R` to `S` that preserve the star operation, i.e., for any `f : F` and `r ∈ R`, we have `f (star r) = star (f r)`. Here, `R` and `S` are types equipped with star operations (involutions), and `F` is a function-like type that respects these operations.
Units.instStarMul instance
: StarMul Rˣ
Full source 
instance : StarMul Rˣ where
  star u :=
    { val := star u
      inv := star ↑u⁻¹
      val_inv := (star_mul _ _).symm.trans <| (congr_arg star u.inv_val).trans <| star_one _
      inv_val := (star_mul _ _).symm.trans <| (congr_arg star u.val_inv).trans <| star_one _ }
  star_involutive _ := Units.ext (star_involutive _)
  star_mul _ _ := Units.ext (star_mul _ _)
Star Multiplication Structure on Units of a Monoid
Informal description
For any monoid $R$ equipped with a star operation, the group of units $R^\times$ inherits a star multiplication structure where the star operation is defined component-wise and satisfies $\star(u \cdot v) = \star v \cdot \star u$ for all units $u, v \in R^\times$.
Units.coe_star theorem
(u : Rˣ) : ↑(star u) = (star ↑u : R)
Full source 
@[simp]
theorem coe_star (u : Rˣ) : ↑(star u) = (star ↑u : R) :=
  rfl
Star Operation Commutes with Unit Inclusion
Informal description
For any unit $u$ in the group of units $R^\times$ of a monoid $R$ equipped with a star operation, the canonical inclusion map $\uparrow$ satisfies $\uparrow(\star u) = \star(\uparrow u)$ in $R$.
Units.coe_star_inv theorem
(u : Rˣ) : ↑(star u)⁻¹ = (star ↑u⁻¹ : R)
Full source 
@[simp]
theorem coe_star_inv (u : Rˣ) : ↑(star u)⁻¹ = (star ↑u⁻¹ : R) :=
  rfl
Star and Inverse Commute for Units: $(u^*)^{-1} = (u^{-1})^*$
Informal description
For any unit $u$ in the group of units $R^\times$ of a monoid $R$ equipped with a star operation, the canonical inclusion of the inverse of the star of $u$ into $R$ equals the star of the canonical inclusion of the inverse of $u$ into $R$, i.e., $(u^*)^{-1} = (u^{-1})^*$ where $*$ denotes the star operation.
Units.instStarModule instance
{A : Type*} [Star A] [SMul R A] [StarModule R A] : StarModule Rˣ A
Full source 
instance {A : Type*} [Star A] [SMul R A] [StarModule R A] : StarModule Rˣ A :=
  ⟨fun u a => star_smul (u : R) a⟩
Star Module Structure on Units of a Monoid
Informal description
For any monoid $R$ equipped with a star operation and any type $A$ with a star operation and a scalar multiplication action by $R$ that is compatible with the star operations (i.e., $\star(r \cdot a) = \star r \cdot \star a$ for all $r \in R$ and $a \in A$), the group of units $R^\times$ of $R$ also acts on $A$ via scalar multiplication in a way that respects the star operations.
IsUnit.star theorem
[Monoid R] [StarMul R] {a : R} : IsUnit a → IsUnit (star a)
Full source 
protected theorem IsUnit.star [Monoid R] [StarMul R] {a : R} : IsUnit a → IsUnit (star a)
  | ⟨u, hu⟩ => ⟨Star.star u, hu ▸ rfl⟩
Star preserves units in a star-monoid
Informal description
Let $R$ be a monoid equipped with a star operation $\star$ satisfying $\star(r \cdot s) = \star s \cdot \star r$ for all $r, s \in R$. If an element $a \in R$ is a unit (i.e., invertible), then its star $\star a$ is also a unit.
isUnit_star theorem
[Monoid R] [StarMul R] {a : R} : IsUnit (star a) ↔ IsUnit a
Full source 
@[simp]
theorem isUnit_star [Monoid R] [StarMul R] {a : R} : IsUnitIsUnit (star a) ↔ IsUnit a :=
  ⟨fun h => star_star a ▸ h.star, IsUnit.star⟩
Star Operation Preserves Units: $\text{IsUnit}(\star a) \leftrightarrow \text{IsUnit}(a)$
Informal description
Let $R$ be a monoid equipped with a star operation $\star$ satisfying $\star(r \cdot s) = \star s \cdot \star r$ for all $r, s \in R$. For any element $a \in R$, the star $\star a$ is a unit if and only if $a$ is a unit.
Ring.inverse_star theorem
[Semiring R] [StarRing R] (a : R) : Ring.inverse (star a) = star (Ring.inverse a)
Full source 
theorem Ring.inverse_star [Semiring R] [StarRing R] (a : R) :
    Ring.inverse (star a) = star (Ring.inverse a) := by
  by_cases ha : IsUnit a
  · obtain ⟨u, rfl⟩ := ha
    rw [Ring.inverse_unit, ← Units.coe_star, Ring.inverse_unit, ← Units.coe_star_inv]
  rw [Ring.inverse_non_unit _ ha, Ring.inverse_non_unit _ (mt isUnit_star.mp ha), star_zero]
Star Operation Commutes with Ring Inverse: $\text{inverse}(\star a) = \star(\text{inverse}(a))$
Informal description
Let $R$ be a semiring equipped with a star operation $\star$ making it a *-ring. For any element $a \in R$, the inverse of the star of $a$ equals the star of the inverse of $a$, i.e., \[ \text{Ring.inverse}(\star a) = \star(\text{Ring.inverse}(a)). \]
Invertible.star instance
{R : Type*} [MulOneClass R] [StarMul R] (r : R) [Invertible r] : Invertible (star r)
Full source 
protected instance Invertible.star {R : Type*} [MulOneClass R] [StarMul R] (r : R) [Invertible r] :
    Invertible (star r) where
  invOf := Star.star (⅟ r)
  invOf_mul_self := by rw [← star_mul, mul_invOf_self, star_one]
  mul_invOf_self := by rw [← star_mul, invOf_mul_self, star_one]
Invertibility under Star Operation
Informal description
For any type $R$ with a multiplicative identity and a star operation that is compatible with multiplication, if an element $r \in R$ has a two-sided multiplicative inverse, then its star $\star r$ also has a two-sided multiplicative inverse.
star_invOf theorem
{R : Type*} [Monoid R] [StarMul R] (r : R) [Invertible r] [Invertible (star r)] : star (⅟ r) = ⅟ (star r)
Full source 
theorem star_invOf {R : Type*} [Monoid R] [StarMul R] (r : R) [Invertible r]
    [Invertible (star r)] : star (⅟ r) = ⅟ (star r) := by
  have : star (⅟ r) = star (⅟ r) * ((star r) * ⅟ (star r)) := by
    simp only [mul_invOf_self, mul_one]
  rw [this, ← mul_assoc]
  have : (star (⅟ r)) * (star r) = star 1 := by rw [← star_mul, mul_invOf_self]
  rw [this, star_one, one_mul]
Star Operation Commutes with Inversion: $\star(⅟r) = ⅟(\star r)$
Informal description
Let $R$ be a monoid equipped with a star operation $\star$ satisfying $\star(r \cdot s) = \star s \cdot \star r$ for all $r, s \in R$. For any invertible element $r \in R$ (with two-sided inverse $⅟r$), the star of the inverse of $r$ equals the inverse of the star of $r$, i.e., \[ \star(⅟r) = ⅟(\star r). \]
IsLeftRegular.star theorem
[Mul R] [StarMul R] {x : R} (hx : IsLeftRegular x) : IsRightRegular (star x)
Full source 
protected theorem IsLeftRegular.star [Mul R] [StarMul R] {x : R} (hx : IsLeftRegular x) :
    IsRightRegular (star x) :=
  fun a b h => star_injective <| hx <| by simpa using congr_arg Star.star h
Star Operation Maps Left Regular Elements to Right Regular Elements
Informal description
Let $R$ be a type equipped with a multiplication operation and a star operation $\star$ satisfying $\star(r \cdot s) = \star s \cdot \star r$ for all $r, s \in R$. If an element $x \in R$ is left regular (i.e., left multiplication by $x$ is injective), then $\star x$ is right regular (i.e., right multiplication by $\star x$ is injective).
IsRightRegular.star theorem
[Mul R] [StarMul R] {x : R} (hx : IsRightRegular x) : IsLeftRegular (star x)
Full source 
protected theorem IsRightRegular.star [Mul R] [StarMul R] {x : R} (hx : IsRightRegular x) :
    IsLeftRegular (star x) :=
  fun a b h => star_injective <| hx <| by simpa using congr_arg Star.star h
Star Operation Preserves Right Regularity to Left Regularity
Informal description
Let $R$ be a type equipped with a multiplication operation and a star operation satisfying $\star(r \cdot s) = \star s \cdot \star r$ for all $r, s \in R$. If an element $x \in R$ is right regular (i.e., right multiplication by $x$ is injective), then the star of $x$ is left regular (i.e., left multiplication by $\star x$ is injective).
IsRegular.star theorem
[Mul R] [StarMul R] {x : R} (hx : IsRegular x) : IsRegular (star x)
Full source 
protected theorem IsRegular.star [Mul R] [StarMul R] {x : R} (hx : IsRegular x) :
    IsRegular (star x) :=
  ⟨hx.right.star, hx.left.star⟩
Star Operation Preserves Regularity
Informal description
Let $R$ be a type equipped with a multiplication operation and a star operation $\star$ satisfying $\star(r \cdot s) = \star s \cdot \star r$ for all $r, s \in R$. If an element $x \in R$ is regular (i.e., both left and right multiplication by $x$ are injective), then $\star x$ is also regular.
isRightRegular_star_iff theorem
[Mul R] [StarMul R] {x : R} : IsRightRegular (star x) ↔ IsLeftRegular x
Full source 
@[simp]
theorem isRightRegular_star_iff [Mul R] [StarMul R] {x : R} :
    IsRightRegularIsRightRegular (star x) ↔ IsLeftRegular x :=
  ⟨fun h => star_star x ▸ h.star, (·.star)⟩
Equivalence of Right Regularity of $\star x$ and Left Regularity of $x$
Informal description
For any element $x$ in a type $R$ equipped with a multiplication operation and a star operation $\star$ satisfying $\star(r \cdot s) = \star s \cdot \star r$ for all $r, s \in R$, the star of $x$ is right regular if and only if $x$ is left regular. In other words, $\star x$ is right regular (right multiplication by $\star x$ is injective) precisely when $x$ is left regular (left multiplication by $x$ is injective).
isLeftRegular_star_iff theorem
[Mul R] [StarMul R] {x : R} : IsLeftRegular (star x) ↔ IsRightRegular x
Full source 
@[simp]
theorem isLeftRegular_star_iff [Mul R] [StarMul R] {x : R} :
    IsLeftRegularIsLeftRegular (star x) ↔ IsRightRegular x :=
  ⟨fun h => star_star x ▸ h.star, (·.star)⟩
Equivalence of Left Regularity of $\star x$ and Right Regularity of $x$ in Star-Multiplicative Structures
Informal description
Let $R$ be a type equipped with a multiplication operation and a star operation $\star$ satisfying $\star(r \cdot s) = \star s \cdot \star r$ for all $r, s \in R$. For any element $x \in R$, the star of $x$ is left regular (i.e., left multiplication by $\star x$ is injective) if and only if $x$ is right regular (i.e., right multiplication by $x$ is injective).
isRegular_star_iff theorem
[Mul R] [StarMul R] {x : R} : IsRegular (star x) ↔ IsRegular x
Full source 
@[simp]
theorem isRegular_star_iff [Mul R] [StarMul R] {x : R} :
    IsRegularIsRegular (star x) ↔ IsRegular x := by
  rw [isRegular_iff, isRegular_iff, isRightRegular_star_iff, isLeftRegular_star_iff, and_comm]
Equivalence of Regularity of $\star x$ and $x$ in Star-Multiplicative Structures
Informal description
Let $R$ be a type equipped with a multiplication operation and a star operation $\star$ satisfying $\star(r \cdot s) = \star s \cdot \star r$ for all $r, s \in R$. For any element $x \in R$, the star of $x$ is regular (i.e., both left and right multiplication by $\star x$ are injective) if and only if $x$ is regular (i.e., both left and right multiplication by $x$ are injective).
MulOpposite.instStar instance
[Star R] : Star Rᵐᵒᵖ
Full source 
/-- The opposite type carries the same star operation. -/
instance [Star R] : Star Rᵐᵒᵖ where star r := op (star r.unop)
Star Operation on the Multiplicative Opposite
Informal description
For any type $R$ equipped with a star operation, the multiplicative opposite $R^\text{op}$ inherits a star operation defined by $\text{op}(r)^* = \text{op}(r^*)$ for all $r \in R$.
MulOpposite.unop_star theorem
[Star R] (r : Rᵐᵒᵖ) : unop (star r) = star (unop r)
Full source 
@[simp]
theorem unop_star [Star R] (r : Rᵐᵒᵖ) : unop (star r) = star (unop r) :=
  rfl
Compatibility of Star Operation with Multiplicative Opposite Projection
Informal description
For any type $R$ equipped with a star operation and any element $r$ in the multiplicative opposite $R^\text{op}$, the canonical projection of the star of $r$ equals the star of the canonical projection of $r$. That is, $\text{unop}(r^*) = (\text{unop}(r))^*$.
MulOpposite.op_star theorem
[Star R] (r : R) : op (star r) = star (op r)
Full source 
@[simp]
theorem op_star [Star R] (r : R) : op (star r) = star (op r) :=
  rfl
Star Operation Commutes with Multiplicative Opposite Embedding
Informal description
For any element $r$ in a type $R$ equipped with a star operation, the canonical embedding of the star of $r$ into the multiplicative opposite of $R$ equals the star of the canonical embedding of $r$. That is, $\text{op}(r^*) = (\text{op}(r))^*$.
MulOpposite.instInvolutiveStar instance
[InvolutiveStar R] : InvolutiveStar Rᵐᵒᵖ
Full source 
instance [InvolutiveStar R] : InvolutiveStar Rᵐᵒᵖ where
  star_involutive r := unop_injective (star_star r.unop)
Involutive Star Operation on the Multiplicative Opposite
Informal description
For any type $R$ with an involutive star operation, the multiplicative opposite $R^\text{op}$ also has an involutive star operation, defined by $\text{op}(r)^* = \text{op}(r^*)$ for all $r \in R$.
MulOpposite.instStarMul instance
[Mul R] [StarMul R] : StarMul Rᵐᵒᵖ
Full source 
instance [Mul R] [StarMul R] : StarMul Rᵐᵒᵖ where
  star_mul x y := unop_injective (star_mul y.unop x.unop)
Star Operation on the Multiplicative Opposite of a *-magma
Informal description
For any type $R$ equipped with a multiplication operation and a star operation satisfying the property $\star(r \cdot s) = \star s \cdot \star r$ for all $r, s \in R$, the multiplicative opposite $R^\text{op}$ also inherits a star operation that satisfies the same property.
MulOpposite.instStarAddMonoid instance
[AddMonoid R] [StarAddMonoid R] : StarAddMonoid Rᵐᵒᵖ
Full source 
instance [AddMonoid R] [StarAddMonoid R] : StarAddMonoid Rᵐᵒᵖ where
  star_add x y := unop_injective (star_add x.unop y.unop)
Star Additive Monoid Structure on the Multiplicative Opposite
Informal description
For any additive monoid $R$ equipped with a star additive monoid structure, the multiplicative opposite $R^\text{op}$ also inherits a star additive monoid structure. The star operation on $R^\text{op}$ is defined by $\text{op}(r)^* = \text{op}(r^*)$ for all $r \in R$, and it preserves addition in $R^\text{op}$.
MulOpposite.instStarRing instance
[NonUnitalSemiring R] [StarRing R] : StarRing Rᵐᵒᵖ
Full source 
instance [NonUnitalSemiring R] [StarRing R] : StarRing Rᵐᵒᵖ where
  star_add x y := unop_injective (star_add x.unop y.unop)
Star Ring Structure on the Multiplicative Opposite of a Non-Unital Semiring
Informal description
For any non-unital semiring $R$ equipped with a star ring structure, the multiplicative opposite $R^\text{op}$ also inherits a star ring structure.
MulOpposite.instStarModule instance
{M : Type*} [Star R] [Star M] [SMul R M] [StarModule R M] : StarModule R Mᵐᵒᵖ
Full source 
instance {M : Type*} [Star R] [Star M] [SMul R M] [StarModule R M] :
    StarModule R Mᵐᵒᵖ where
  star_smul r x := unop_injective (star_smul r x.unop)
Star Module Structure on the Multiplicative Opposite
Informal description
For any type $M$ equipped with a star operation and a scalar multiplication by $R$, if $M$ is a star module over $R$, then the multiplicative opposite $M^\text{op}$ is also a star module over $R$. The star operation on $M^\text{op}$ is defined by $\text{op}(m)^* = \text{op}(m^*)$ for all $m \in M$, and the scalar multiplication satisfies $r \cdot \text{op}(m) = \text{op}(r \cdot m)$ for all $r \in R$ and $m \in M$.
StarSemigroup.toOpposite_starModule instance
[CommMonoid R] [StarMul R] : StarModule Rᵐᵒᵖ R
Full source 
/-- A commutative star monoid is a star module over its opposite via
`Monoid.toOppositeMulAction`. -/
instance StarSemigroup.toOpposite_starModule [CommMonoid R] [StarMul R] :
    StarModule Rᵐᵒᵖ R :=
  ⟨fun r s => star_mul' s r.unop⟩
Commutative Star Monoid as Star Module over its Opposite
Informal description
For any commutative monoid $R$ equipped with a star operation that preserves multiplication (i.e., $\star(x \cdot y) = \star x \cdot \star y$ for all $x, y \in R$), $R$ is a star module over its multiplicative opposite $R^\text{op}$ via the right multiplication action.