Theorems · Definition · group theory
Units.mk0
{G₀ : Type u_3} → [inst : GroupWithZero G₀] → (a : G₀) → a ≠ 0 → G₀ˣEmbed a non-zero element of a GroupWithZero into the unit group.
By combining this function with the operations on units,
or the /ₚ operation, it is possible to write a division
as a partial function with three arguments.
- Cited by
- 181 results in Mathlib
- Foundations
- Depth 18 from the axioms, rests on 165 definitions · uses propext, Classical.choice, Quot.sound
- Assumes
- GroupWithZero
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Unitsstatement · cited by 2,804
- GroupWithZerostatement and proof · cited by 691
- inv_mul_cancel₀proof · cited by 267
- mul_inv_cancel₀proof · cited by 210
Cited by201
Results whose statement or proof uses this declaration.
- inv_smul_smul₀proof · cited by 80
- smul_inv_smul₀proof · cited by 59
- IsUnit.mk0proof · cited by 33
- MonoidWithZeroHom.ValueGroup₀.restrict₀proof · cited by 32
- Set.mem_smul_set_iff_inv_smul_mem₀proof · cited by 28
- Units.mk0_valstatement · cited by 19
- Units.mk0.congr_simpstatement and proof · cited by 17
- Units.val_mk0statement · cited by 16
- FractionalIdeal.mk0proof · cited by 13
- MonoidWithZeroHom.ValueGroup₀.restrict₀_applystatement · cited by 13
- Set.mem_inv_smul_set_iff₀proof · cited by 13
- MonoidWithZeroHom.ValueGroup₀.embedding_restrict₀proof · cited by 12
Showing the 200 most cited of 201.