desc_var — Mathlib

English

In the core form, applying the described reduction to a variable g yields that the desconstructed map sends solution.var g to s.var g.

Русский

В ядре через desc_var отображение даёт, что применённая к переменной g функция desc отправляет solution.var g в s.var g.

LaTeX

$$$$ h.desc s (solution.var g) = s.var g $$$$

Lean4

@[simp]
theorem desc_var (h : IsPresentationCore.{w'} solution) {N : Type w'} [AddCommGroup N] [Module A N]
    (s : relations.Solution N) (g : relations.G) : h.desc s (solution.var g) = s.var g :=
  congr_var (h.postcomp_desc s) g

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