congrLinearEquiv — Mathlib

English

A semilinear equivalence e12: M1 ≃ₛₗ[σ12] M2 induces a group isomorphism between general linear groups: congrLinearEquiv e12 : GeneralLinearGroup R1 M1 ≃* GeneralLinearGroup R2 M2.

Русский

Семилинейное эквивалентность e12: M1 ≃ₛₗ[σ12] M2 порождает изоморфизм между группами общих линейных преобразований: congrLinearEquiv e12 : GeneralLinearGroup R1 M1 ≃* GeneralLinearGroup R2 M2.

LaTeX

$$$ congrLinearEquiv\; (e_{12}) : GeneralLinearGroup R_1 M_1 \cong* GeneralLinearGroup R_2 M_2. $$$

Lean4

/-- A semilinear equivalence from `V` to `W` determines an isomorphism of general linear
groups. -/
def congrLinearEquiv (e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂) : GeneralLinearGroup R₁ M₁ ≃* GeneralLinearGroup R₂ M₂ :=
  Units.mapEquiv (LinearEquiv.conjRingEquiv e₁₂).toMulEquiv

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