Theorems · Theorem · group theory
MonoidWithZeroHom.mem_valueGroup_iff_of_comm
∀ {A : Type u_1} {B : Type u_2} [inst : MonoidWithZero A] [inst_1 : CommGroupWithZero B] (f : A →*₀ B) {y : Bˣ},
y ∈ f.valueGroup ↔ ∃ a, f a ≠ 0 ∧ ∃ x, f a * ↑y = f xSee also mem_valueGroup_iff_of_comm' for a version proving that f x ≠ 0.
- Defined in
- Mathlib.Algebra.GroupWithZero.Range
- Cited by
- 3 results in Mathlib
- Foundations
- Depth 71 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites27
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
- SetLike.coeproof · cited by 8,199
- Set.preimageproof · cited by 4,946
- Set.rangeproof · cited by 4,705
- mul_oneproof · cited by 3,885
- Subgroupstatement · cited by 3,593
- Unitsstatement and proof · cited by 2,804
- Units.valstatement and proof · cited by 1,966
- map_mulproof · cited by 1,137
- map_oneproof · cited by 861
- MonoidWithZeroHomstatement and proof · cited by 704
- MonoidWithZerostatement and proof · cited by 456
Cited by3
Results whose statement or proof uses this declaration.
- Valuation.exists_div_eq_of_unitproof · cited by 2
- Valuation.IsEquiv.uniformContinuousproof · cited by 1
- MonoidWithZeroHom.mem_valueGroup_iff_of_comm'proof · cited by 1