baseChange_toGenerators — Mathlib

English

The comparison of generators under base change holds: (P.baseChange T).toGenerators = P.toGenerators.baseChange T.

Русский

Сопоставление генераторов при базовом изменении выполняется: (P.baseChange T).toGenerators = P.toGenerators.baseChange T.

LaTeX

$$$\\mathrm{baseChange}\\;\\text{toGenerators}: (P.baseChange\\ T).toGenerators = P.toGenerators.baseChange\\ T$$$

Lean4

theorem baseChange_toGenerators : (P.baseChange T).toGenerators = P.toGenerators.baseChange T :=
  rfl

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