Theorems · Theorem · group theory
map_dvd
∀ {M : Type u_1} {N : Type u_2} [inst : Semigroup M] [inst_1 : Semigroup N] {F : Type u_3} [inst_2 : FunLike F M N]
[MulHomClass F M N] (f : F) {a b : M}, a ∣ b → f a ∣ f b- Defined in
- Mathlib.Algebra.Divisibility.Hom
- Cited by
- 44 results in Mathlib
- Foundations
- Depth 6 from the axioms · uses no axioms
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.
- DFunLike.coestatement and proof · cited by 62,936
- FunLikestatement and proof · cited by 2,560
- map_mulproof · cited by 1,137
- Semigroupstatement and proof · cited by 202
- MulHomClassstatement and proof · cited by 73
Cited by44
Results whose statement or proof uses this declaration.
- Polynomial.map_dvdproof · cited by 10
- Ideal.spanNorm_singletonproof · cited by 5
- Ideal.absNorm_dvd_absNorm_of_leproof · cited by 5
- IsAlgebraic.exists_nonzero_dvdproof · cited by 5
- map_dvd_iffproof · cited by 3
- comap_primeproof · cited by 3
- MvPolynomial.dvd_monomial_iff_existsproof · cited by 3
- exists_bijective_map_powersproof · cited by 3
- Nat.cast_dvd_castproof · cited by 3
- Matrix.isUnit_charpolyRev_of_isNilpotentproof · cited by 2
- IsLocalization.of_le_of_exists_dvdproof · cited by 2
- HomogeneousLocalization.val_awayMapstatement and proof · cited by 2