mk'_eq_of_same — Mathlib

English

Let a,b ∈ M and d ∈ S. Then f.mk' a d = f.mk' b d if and only if there exists c ∈ S with c a = c b.

Русский

Пусть a,b ∈ M и d ∈ S. Тогда f.mk' a d = f.mk' b d тогда и только тогда существует c ∈ S с c a = c b.

LaTeX

$$$ f.mk' a d = f.mk' b d \\iff \\exists c \\in S, c a = c b $$$

Lean4

@[to_additive]
theorem mk'_eq_of_same {a b} {d : S} : f.mk' a d = f.mk' b d ↔ ∃ c : S, c * a = c * b :=
  by
  rw [mk'_eq_iff_eq', map_mul, map_mul, ← eq_iff_exists f]
  exact (map_units f d).mul_left_inj

Похожие утверждения