domLCongr_refl — Mathlib

English

If you apply domLCongr with the identity, you get the identity on the space of alternating maps.

Русский

Если применить domLCongr с тождественным отображением, то получаем тождественное отображение на пространстве чередующихся карт.

LaTeX

$$domLCongr(R,N,ι,S)(LinearEquiv.refl R M) = LinearEquiv.refl S (AlternatingMap R M N ι)$$

Lean4

@[simp]
theorem domLCongr_refl : domLCongr R N ι S (LinearEquiv.refl R M) = LinearEquiv.refl S _ :=
  LinearEquiv.ext fun _ => AlternatingMap.ext fun _ => rfl

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