div_surjective — Mathlib

English

For any z in K there exist a,b in A with b a nonZeroDivisor such that algebraMap a / algebraMap b represents z.

Русский

Для любого z ∈ K существуют a,b ∈ A с b ∈ nonZeroDivisors(A), такие что z = algebraMap(a)/algebraMap(b).

LaTeX

$$∃ x,y ∈ A, y ∈ nonZeroDivisors(A) ∧ algebraMap _ _ x / algebraMap _ _ y = z$$

Lean4

theorem div_surjective (z : K) : ∃ x y : A, y ∈ nonZeroDivisors A ∧ algebraMap _ _ x / algebraMap _ _ y = z :=
  let ⟨x, ⟨y, hy⟩, h⟩ := mk'_surjective (nonZeroDivisors A) z
  ⟨x, y, hy, by rwa [mk'_eq_div] at h⟩

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