The star operation, bundled as a star-linear equiv #
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. We only the commutative case for now since, in the noncommutative case, the ring hom needs to reverse the order of multiplication. This requires a ring hom of type
R →+* Rᵐᵒᵖ, which is very undesirable in the commutative case. One way out would be to define a new typeclass
is_op R Sand have an instance
is_op R Rfor commutative
- Also note that such a definition involving
is_op R Swould require adding the appropriate
ring_hom_inv_pairinstances to be able to define the semilinear equivalence.
A is a module over a commutative
R with compatible actions,
star is a semilinear equivalence.