liftOn_def — Mathlib

English

For the construction x = ofFractionRing(Localization.mk n d), the liftOn evaluated at f agrees with f(n,d).

Русский

Для x = ofFractionRing(Localization.mk n d) функции liftOn дают f(n,d).

LaTeX

$$$\\text{liftOn} (\\mathrm{ofFractionRing}(\\mathrm{Localization.mk}\\, n\, d))\, f \\, = \\, f(n,d)$$$

Lean4

theorem liftOn_def : eta_helper Eq✝ @liftOn.{} @(delta% @definition✝) :=
  by
  intros
  delta liftOn
  rw [show wrapped✝ = ⟨@definition✝.{}, rfl✝⟩ from Subtype.ext✝ wrapped✝.2.symm✝]
  rfl

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