linearEquiv_symm_apply — Mathlib

English

Let S be a submonoid as above. Then the inverse of the localization linear equivalence satisfies (linearEquiv S f g).symm (g x) = f x for all x ∈ M.

Русский

Пусть S — подмоноид; тогда обратное линейного эквивалента локализации выполняется: (linearEquiv S f g).symm (g x) = f x для всех x ∈ M.

LaTeX

$$$\\forall x \\in M:\\ (\\mathrm{linearEquiv}\\ S\\ f\\ g).\\mathrm{symm}}(g\\,x) = f\\,x$$$

Lean4

@[simp]
theorem linearEquiv_symm_apply [IsLocalizedModule S g] (x : M) : (linearEquiv S f g).symm (g x) = f x := by
  simp [linearEquiv]

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