English
The auxiliary lemmas assert basic compatibility of star with addition, scalar action, and inverses inside the star-linear framework.
Русский
Дополнительные леммы подтверждают базовую совместимость звезды с дествиями сложения, скаляра и обратными в рамках звездо-линией.
LaTeX
$$$\text{(compatibility statements for starLinearEquiv)}$$$
Lean4
/-- If `A` is a module over a commutative `R` with compatible actions,
then `star` is a semilinear equivalence. -/
@[simps]
def starLinearEquiv (R : Type*) {A : Type*} [CommSemiring R] [StarRing R] [AddCommMonoid A] [StarAddMonoid A]
[Module R A] [StarModule R A] : A ≃ₗ⋆[R] A :=
{ starAddEquiv with
toFun := star
map_smul' := star_smul }
