exists_gen_dvd_sub — Mathlib

English

Let pb be a power basis of B over A. Then there exists a in A such that pb.gen divides b − algebraMap_A_B(a) in B.

Русский

Пусть pb является базисом мощности для B над A. Тогда существует a в A такое, что pb.gen делит b − algebraMap_A_B(a) в B.

LaTeX

$$$\exists a\in A\; pb.gen \mid (b - \text{algebraMap}_A^B(a))$$$

Lean4

theorem exists_gen_dvd_sub (pb : PowerBasis A B) (b : B) : ∃ a, pb.gen ∣ b - algebraMap A B a := by
  simpa [← Ideal.mem_span_singleton, ← mk_eq_zero, mk_sub, sub_eq_zero] using pb.exists_smodEq b

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