Theorems · Inductive type · ring theory
InvolutiveStar
Type u → Type u
Typeclass for a star operation with is involutive.
- Defined in
- Mathlib.Algebra.Star.Basic
- Cited by
- 52 results in Mathlib
- Foundations
- Depth 0 from the axioms · uses no axioms
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 by73
Results whose statement or proof uses this declaration.
- star_starstatement and proof · cited by 135
- Matrix.conjTranspose_conjTransposestatement and proof · cited by 31
- InvolutiveStar.star_involutivestatement and proof · cited by 11
- star_injectivestatement and proof · cited by 8
- star_eq_iff_star_eqstatement and proof · cited by 6
- StarMemClass.star_coe_eqstatement and proof · cited by 5
- Equiv.Perm.starstatement and proof · cited by 4
- Matrix.conjTranspose_involutivestatement and proof · cited by 4
- Matrix.conjTranspose_injstatement and proof · cited by 2
- Set.star_mem_starstatement and proof · cited by 2
- IsSelfAdjoint.star_iffstatement and proof · cited by 2
- Equiv.Perm.star_applystatement and proof · cited by 1