Theorems · Definition · group theory
MonoidWithZeroHom.valueGroup.mk
{A : Type u_1} →
{B : Type u_2} →
[inst : MonoidWithZero A] →
[inst_1 : CommGroupWithZero B] → (f : A →*₀ B) → (r s : A) → f r ≠ 0 → f s ≠ 0 → ↥f.valueGroupThe map sending a pair of nonzero r s : A to the element (v r)⁻¹ * (v s)
of ValueGroup₀ v.
- Defined in
- Mathlib.Algebra.GroupWithZero.Range
- Cited by
- 11 results in Mathlib
- Foundations
- Depth 70 from the axioms · uses propext, Classical.choice, 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.
- DFunLike.coestatement and proof · cited by 62,936
- Subgroupstatement · cited by 3,593
- Unitsstatement · cited by 2,804
- MonoidWithZeroHomstatement and proof · cited by 704
- MonoidWithZerostatement and proof · cited by 456
- Units.mk0proof · cited by 181
- MonoidWithZeroHom.valueGroupstatement · cited by 170
- CommGroupWithZerostatement and proof · cited by 94
Cited by13
Results whose statement or proof uses this declaration.
- Valuation.IsEquiv.valueGroup₀Funproof · cited by 4
- MonoidWithZeroHom.ValueGroup₀.zero_or_exists_mkstatement · cited by 3
- Valuation.IsEquiv.valueGroup₀Fun_specstatement and proof · cited by 3
- Valuation.IsEquiv.orderMonoidIso_specproof · cited by 2
- Valuation.restrict_eq_mkstatement · cited by 1
- MonoidWithZeroHom.ValueGroup₀.mkproof · cited by 1
- MonoidWithZeroHom.valueGroup.mk.congr_simpstatement and proof · cited by 1
- Valuation.IsEquiv.orderMonoidIso_transproof · cited by 0
- MonoidWithZeroHom.ValueGroup₀.mk_eq_of_ne_zerostatement and proof · cited by 0
- MonoidWithZeroHom.valueGroup.mk_injstatement · cited by 0
- MonoidWithZeroHom.valueGroup.mk_mulstatement · cited by 0
- MonoidWithZeroHom.ValueGroup₀.zero_or_exists_mk'statement and proof · cited by 0