mk'_eq_div — Mathlib

English

The canonical mk' representation equals the division of images under the algebra map.

Русский

Стандартное представление mk' равно делению образов через алгебраическое отображение.

LaTeX

$$mk'_eq_div {r} (s : nonZeroDivisors A) : mk' K r ⟨s, hs⟩ = algebraMap A K r / algebraMap A K s$$

Lean4

@[simp]
theorem mk'_eq_div {r} (s : nonZeroDivisors A) : mk' K r s = algebraMap A K r / algebraMap A K s :=
  mk'_mk_eq_div s.2

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