Theorems · Theorem · commutative algebra

map_dvd_iff

∀ {α : Type u_1} {β : Type u_2} [inst : Semigroup α] [inst_1 : Semigroup β] {F : Type u_3} [inst_2 : EquivLike F α β]
  [MulEquivClass F α β] (f : F) {a b : α}, f a ∣ f b ↔ a ∣ b

Defined in

Mathlib.Algebra.Ring.Divisibility.Basic

Cited by

3 results in Mathlib

Foundations

Depth 18 from the axioms · uses Quot.sound

Assumes

SemigroupSemigroupEquivLikeMulEquivClass