Theorems · Theorem · ring theory
Unitary.mul_inv_mem_iff
∀ {G : Type u_2} [inst : Group G] [inst_1 : StarMul G] (a b : G), a * b⁻¹ ∈ unitary G ↔ star a * a = star b * b- Defined in
- Mathlib.Algebra.Star.Unitary
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 27 from the axioms · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites13
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Groupstatement and proof · cited by 6,238
- mul_oneproof · cited by 3,885
- Submonoidstatement · cited by 3,086
- mul_assocproof · cited by 1,667
- Star.starstatement and proof · cited by 1,082
- unitarystatement · cited by 207
- StarMulstatement and proof · cited by 195
- StarMul.star_mulproof · cited by 72
- Group.isUnitproof · cited by 18
- mul_inv_eq_iff_eq_mulproof · cited by 13
- star_invproof · cited by 6
- inv_mul_eq_iff_eq_mulproof · cited by 5
Cited by1
Results whose statement or proof uses this declaration.
- Unitary.inv_mul_mem_iffproof · cited by 0