Theorems · Definition · ring theory
Unitary.toUnits
{R : Type u_1} → [inst : Monoid R] → [inst_1 : StarMul R] → ↥(unitary R) →* RˣThe unitary elements embed into the units.
- Defined in
- Mathlib.Algebra.Star.Unitary
- Cited by
- 18 results in Mathlib
- Foundations
- Depth 29 from the axioms · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites8
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Monoidstatement and proof · cited by 3,887
- MonoidHomstatement · cited by 3,629
- Submonoidstatement · cited by 3,086
- Unitsstatement · cited by 2,804
- unitarystatement and proof · cited by 207
- StarMulstatement and proof · cited by 195
- Unitary.coe_star_mul_selfproof · cited by 4
- Unitary.coe_mul_star_selfproof · cited by 2
Cited by21
Results whose statement or proof uses this declaration.
- Unitary.conjStarAlgAutproof · cited by 26
- Unitary.mulRightproof · cited by 9
- Unitary.val_toUnits_applystatement and proof · cited by 7
- Unitary.mulLeftproof · cited by 7
- Unitary.val_inv_toUnits_applystatement and proof · cited by 4
- Unitary.spectrum_subset_circleproof · cited by 2
- Unitary.isUnit_coeproof · cited by 2
- Unitary.toAlgEquiv_conjStarAlgAutstatement · cited by 0
- Unitary.toLinearEquiv_mulLeftstatement · cited by 0
- Unitary.toLinearEquiv_mulRightstatement · cited by 0
- Unitary.toRingEquiv_conjStarAlgAutstatement · cited by 0
- Unitary.toUnits_comp_mapstatement and proof · cited by 0