instFiniteDimensional — Mathlib

English

If R is a division ring and H is a finite-dimensional free R-module, then Hᵐᵒᵖ is also finite-dimensional over R.

Русский

Если R — делительная кольцо и H — конечномерный свободный R-модуль, то Hᵐᵒᵖ также конечномерный над R.

LaTeX

$$FiniteDimensional R H^{\mathrm{op}}$$

Lean4

instance [DivisionRing R] [AddCommGroup H] [Module R H] [FiniteDimensional R H] : FiniteDimensional R Hᵐᵒᵖ :=
  FiniteDimensional.of_finite_basis (Basis.ofVectorSpace R H).mulOpposite (Basis.ofVectorSpaceIndex R H).toFinite

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