Theorems · Inductive type · ring theory
StarMul
(R : Type u) → [Mul R] → Type u
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
- Cited by
- 195 results in Mathlib
- Foundations
- Depth 1 from the axioms, rests on 2 definitions · uses no axioms
- Assumes
- Mul
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites0
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
Nothing in Mathlib beyond the foundations.
Cited by233
Results whose statement or proof uses this declaration.
- unitarystatement and proof · cited by 207
- StarMul.star_mulstatement and proof · cited by 72
- star_onestatement and proof · cited by 33
- Unitary.conjStarAlgAutstatement and proof · cited by 26
- StarAlgHom.ofIdstatement and proof · cited by 18
- Unitary.toUnitsstatement and proof · cited by 18
- skewAdjointPartstatement and proof · cited by 15
- IsCHSHTuplestatement · cited by 14
- Unitary.star_mul_self_of_memstatement and proof · cited by 13
- IsSelfAdjoint.star_mul_selfstatement and proof · cited by 12
- IsUnit.starstatement and proof · cited by 11
- Unitary.mapstatement and proof · cited by 10
Showing the 200 most cited of 233.