Theorems · Theorem · group theory
Units.mk0_val
∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] (u : G₀ˣ) (h : ↑u ≠ 0), Units.mk0 (↑u) h = u- Cited by
- 19 results in Mathlib
- Foundations
- Depth 19 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- GroupWithZero
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Unitsstatement and proof · cited by 2,804
- Units.valstatement and proof · cited by 1,966
- GroupWithZerostatement and proof · cited by 691
- Units.mk0statement · cited by 181
- Units.extproof · cited by 86
Cited by19
Results whose statement or proof uses this declaration.
- Valuation.subgroups_basisproof · cited by 5
- MonoidWithZeroHom.fst_inlproof · cited by 3
- MonoidWithZeroHom.snd_inrproof · cited by 3
- MonoidWithZeroHom.ValueGroup₀.zero_or_exists_mkproof · cited by 3
- MonoidWithZeroHom.inl_apply_unitproof · cited by 2
- Valued.integer.locallyFiniteOrder_units_mrange_of_isCompact_integerproof · cited by 2
- MonoidWithZeroHom.fst_comp_inrproof · cited by 1
- MonoidWithZeroHom.snd_comp_inlproof · cited by 1
- MonoidWithZeroHom.inl_monoproof · cited by 1
- Valuation.IsUniformizer.zpowers_eq_valueGroupproof · cited by 1
- LinearOrderedCommGroupWithZero.inl_eq_coe_inlₗproof · cited by 1
- MonoidWithZeroHom.inr_apply_unitproof · cited by 1