congrLinearEquiv_refl — Mathlib

English

Congruence by the identity equivalence equals the identity on the general linear group.

Русский

Конгруэнция по тождественной эквивалентности равна тождественному изоморфизму на группе GL.

LaTeX

$$$ congrLinearEquiv (LinearEquiv.refl R_1 M_1) = MulEquiv.refl (GeneralLinearGroup R_1 M_1) $$$

Lean4

@[simp]
theorem congrLinearEquiv_refl : congrLinearEquiv (LinearEquiv.refl R₁ M₁) = MulEquiv.refl (GeneralLinearGroup R₁ M₁) :=
  rfl

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