map_variableChange — Mathlib

English

Compatibility of map with variable changes: applying the map to a variable change and then acting on W equals applying the variable-change action to W and then mapping.

Русский

Совместимость отображения с изменением переменных: применение отображения к смене переменных и затем действие на W эквивалентно применению смены переменных к W и затем отображению.

LaTeX

$$$$ (C.map\phi) \,\cdot\, (W.map\phi) = (C \cdot W).map\phi $$$$

Lean4

theorem map_variableChange (C : VariableChange R) : (C.map φ) • (W.map φ) = (C • W).map φ :=
  by
  simp only [map, variableChange_def, VariableChange.map]
  ext <;> map_simp <;> simp only [Units.coe_map_inv, MonoidHom.coe_coe]

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