denomsClearable_zero — Mathlib

English

For any N, a, and an invertible bi relative to i(b), DenomsClearable a b N 0 i holds.

Русский

Для любого N, a и би, удовлетворяющего bi · i(b) = 1, выполняется DenomsClearable a b N 0 i.

LaTeX

$$$\forall N\; \forall a\; \forall bu, bu \cdot i(b) = 1 \rightarrow DenomsClearable\ a\ b\ N\ 0\ i$$$

Lean4

theorem denomsClearable_zero (N : ℕ) (a : R) (bu : bi * i b = 1) : DenomsClearable a b N 0 i :=
  ⟨0, bi, bu, by simp only [eval_zero, RingHom.map_zero, mul_zero, Polynomial.map_zero]⟩

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