equiv_symm

Mathlib.LinearAlgebra.Basis.Defs

URI: https://scilib.ai/kg/mathlib#Module.Basis.equiv_symm

English

The constr operation commutes with composition: constr b S (f ∘ v) = f ∘ constr b S v.

Русский

Операция constr сохраняет композицию: constr b S (f ∘ v) = f ∘ constr b S v.

LaTeX

$$$\\mathrm{constr}\\, b\\ S\\ (f \\circ v) = f \\circ \\mathrm{constr}\\, b\\ S\\ v.$$$

Lean4

@[simp]
theorem equiv_symm : (b.equiv b' e).symm = b'.equiv b e.symm :=
  b'.ext' fun i => (b.equiv b' e).injective (by simp)

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru