mathlib documentation

algebra.star.module

The star operation, bundled as a star-linear equiv #

We define star_linear_equiv, which is the star operation bundled as a star-linear map. It is defined on a star algebra A over the base ring R.

TODO #

@[simp]
theorem star_linear_equiv_symm_apply (R : Type u_1) {A : Type u_2} [comm_ring R] [star_ring R] [semiring A] [star_ring A] [module R A] [star_module R A] (ᾰ : A) :
@[simp]
theorem star_linear_equiv_apply (R : Type u_1) {A : Type u_2} [comm_ring R] [star_ring R] [semiring A] [star_ring A] [module R A] [star_module R A] (ᾰ : A) :
def star_linear_equiv (R : Type u_1) {A : Type u_2} [comm_ring R] [star_ring R] [semiring A] [star_ring A] [module R A] [star_module R A] :

If A is a module over a commutative R with compatible actions, then star is a semilinear equivalence.

Equations