Structures · Algebra
StarMul
A \-magma is a magma `R` with an involutive operation `star` such that `star (r s) = star s * star r`.
- Defined in
- Mathlib.Algebra.Star.Basic
- Shape
- One type argument · adds star_mul
Extends1
Extended by1
Concrete types that are instances15
- ContinuousLinearMap
- TensorProduct
- WithConv
- Units
- MeasureTheory.SimpleFunc
- DirectLimit
- FreeMonoid
- MulChar
- Complex.UnitClosedDisc
- Complex.UnitDisc
- Subtype
- Prod
- MulOpposite
- ContinuousMap
- LinearMap
How is a type an instance?
Loading the hierarchy index…
Assumed by250
- unitary
- StarMul.star_mul
- star_one
- Unitary.conjStarAlgAut
- Unitary.toUnits
- StarAlgHom.ofId
- skewAdjointPart
- Unitary.star_mul_self_of_mem
- IsSelfAdjoint.star_mul_self
- IsUnit.star
- Unitary.map
- selfAdjointPart
- selfAdjoint.submodule
- skewAdjointPart_apply_coe
- Unitary.mem_iff
- Unitary.val_toUnits_apply
- starMulEquiv
- star_inv
- StarAlgHom.ofId_apply
- Unitary.mul_star_self_of_mem
- star_inv₀
- Unitary.mapEquiv
- unitarySubgroup
- IsSelfAdjoint.commute_iff
- star_mul'
- selfAdjointPart_apply_coe
- IsRegular.star
- Unitary.val_inv_toUnits_apply
- Unitary.conjStarAlgAut_apply
- IsSelfAdjoint.pow
- Unitary.coe_star_mul_self
- StarModule.decomposeProdAdjoint
- skewAdjoint.submodule
- algebraMap_star_comm
- IsRightRegular.star
- Unitary.mul_star_self
- Unitary.star_mul_self
- Unitary.spectrum_star_right_conjugate
- IsUnit.mem_unitary_iff_star_mul_self
- unitarySubgroupUnitsEquiv
- isStarNormal_of_mem_unitary
- Unitary.star_mem
- Commute.star_left
- starMulAut
- IsLeftRegular.star
- IsSelfAdjoint.one
- IsSelfAdjoint.mul_star_self
- Unitary.coe_inv
- star_invOf
- semiconjBy_star_star_star