expand_contract' — Mathlib

English

For general ExpChar R p, either p = 1, in which case expansion and contraction reduce to identity, or else expand_contract holds as above.

Русский

Для общего ExpChar R p либо p = 1, тогда расширение и сжатие сводятся к тождественному отображению, либо же выполняется expand_contract как выше.

LaTeX

$$$$\mathrm{expand}_R(p)\bigl(\mathrm{contract}_p f\bigr)=f$$$$

Lean4

theorem expand_contract' [NoZeroDivisors R] {f : R[X]} (hf : Polynomial.derivative f = 0) :
    expand R p (contract p f) = f :=
  by
  obtain _ | @⟨_, hprime, hchar⟩ := ‹ExpChar R p›
  · rw [expand_one, contract_one]
  · haveI := Fact.mk hchar; exact expand_contract p hf hprime.ne_zero

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