Transfer star (algebraic) structures across Equivs

This continues the pattern set in Mathlib/Algebra/Group/TransferInstance.lean.

@[reducible, inline]

abbrev Equiv.star {R : Type u_1} {S : Type u_2} (e : R ≃ S) [Star S] : Star R

Transfer Star across an Equiv. See note [reducible non-instances].

For star : R → R bundled as an Equiv, see Equiv.Perm.star.

Equations

• e.star = { star := fun (r : R) => e.symm (star (e r)) }

@[reducible, inline]

abbrev Equiv.involutiveStar {R : Type u_1} {S : Type u_2} (e : R ≃ S) [InvolutiveStar S] : InvolutiveStar R

Transfer InvolutiveStar across an Equiv. See note [reducible non-instances].

Equations

• e.involutiveStar = Function.Injective.involutiveStar ⇑e ⋯ ⋯

@[reducible, inline]

abbrev Equiv.starMul {R : Type u_1} {S : Type u_2} (e : R ≃ S) [Mul S] [StarMul S] : StarMul R

Transfer StarMul across an Equiv. See note [reducible non-instances].

Equations

• e.starMul = Function.Injective.starMul ⇑e ⋯ ⋯ ⋯

@[reducible, inline]

abbrev Equiv.starAddMonoid {R : Type u_1} {S : Type u_2} (e : R ≃ S) [AddMonoid S] [StarAddMonoid S] : StarAddMonoid R

Transfer StarAddMonoid across an Equiv. See note [reducible non-instances].

Equations

• e.starAddMonoid = Function.Injective.starAddMonoid ⇑e ⋯ ⋯ ⋯

@[reducible, inline]

abbrev Equiv.starRing {R : Type u_1} {S : Type u_2} (e : R ≃ S) [NonUnitalNonAssocSemiring S] [StarRing S] : StarRing R

Transfer StarRing across an Equiv. See note [reducible non-instances].

Equations

• e.starRing = Function.Injective.starRing ⇑e ⋯ ⋯ ⋯ ⋯

theorem Equiv.starModule {R : Type u_1} {S : Type u_2} (e : R ≃ S) (𝕜 : Type u_3) [Star 𝕜] [Star S] [SMul 𝕜 S] [StarModule 𝕜 S] : StarModule 𝕜 R

Transfer StarModule across an Equiv