monomial_mem_lifts — Mathlib

English

If s lies in the image of f, then the monomial n·s (i.e., monomial n with coefficient s) lifts.

Русский

Если элемент s принадлежит образу f, то моном X^n · s (мономиал с коэффициентом s) поднимается.

LaTeX

$$$ monomial\, n\, s \in \mathrm{lifts}\ f$$$

Lean4

/-- If `(s : S)` is in the image of `f`, then `monomial n s` lifts. -/
theorem monomial_mem_lifts {s : S} (n : ℕ) (h : s ∈ Set.range f) : monomial n s ∈ lifts f :=
  by
  obtain ⟨r, rfl⟩ := Set.mem_range.1 h
  use monomial n r
  simp only [coe_mapRingHom, map_monomial]

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