ofTop_apply — Mathlib

English

The ofTop equivalence acts as the identity on top elements when evaluated at the top of the submodule.

Русский

Эквивалентность ofTop действует как тождественный отображение на верхнем подмодуле.

LaTeX

$$theorem ofTop_apply (x : (⊤ : LieSubmodule R L M)) : LieModuleEquiv.ofTop R L M x = x$$

Lean4

theorem ofTop_apply (x : (⊤ : LieSubmodule R L M)) : LieModuleEquiv.ofTop R L M x = x :=
  rfl

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