Basis of an opposite space #
This file defines the basis of an opposite space and shows that the opposite space is finite-dimensional and free when the original space is.
noncomputable def
Module.Basis.mulOpposite
{R : Type u_1}
{H : Type u_2}
{ι : Type u_3}
[Semiring R]
[AddCommMonoid H]
[Module R H]
(b : Basis ι R H)
:
The multiplicative opposite of a basis: b.mulOpposite i ↦ op (b i).
Equations
- b.mulOpposite = b.map (MulOpposite.opLinearEquiv R)
Instances For
@[simp]
theorem
Module.Basis.mulOpposite_apply
{R : Type u_1}
{H : Type u_2}
{ι : Type u_3}
[Semiring R]
[AddCommMonoid H]
[Module R H]
(b : Basis ι R H)
(i : ι)
:
theorem
Module.Basis.mulOpposite_repr_eq
{R : Type u_1}
{H : Type u_2}
{ι : Type u_3}
[Semiring R]
[AddCommMonoid H]
[Module R H]
(b : Basis ι R H)
:
@[simp]
theorem
Module.Basis.repr_unop_eq_mulOpposite_repr
{R : Type u_1}
{H : Type u_2}
{ι : Type u_3}
[Semiring R]
[AddCommMonoid H]
[Module R H]
(b : Basis ι R H)
(x : Hᵐᵒᵖ)
:
@[simp]
theorem
Module.Basis.mulOpposite_repr_op
{R : Type u_1}
{H : Type u_2}
{ι : Type u_3}
[Semiring R]
[AddCommMonoid H]
[Module R H]
(b : Basis ι R H)
(x : H)
:
instance
MulOpposite.instFiniteDimensional
{R : Type u_1}
{H : Type u_2}
[DivisionRing R]
[AddCommGroup H]
[Module R H]
[FiniteDimensional R H]
:
instance
MulOpposite.instFree
{R : Type u_1}
{H : Type u_2}
[Semiring R]
[AddCommMonoid H]
[Module R H]
[Module.Free R H]
:
Module.Free R Hᵐᵒᵖ
theorem
MulOpposite.rank
{R : Type u_1}
{H : Type u_2}
[Semiring R]
[StrongRankCondition R]
[AddCommMonoid H]
[Module R H]
[Module.Free R H]
:
theorem
MulOpposite.finrank
{R : Type u_1}
{H : Type u_2}
[DivisionRing R]
[AddCommGroup H]
[Module R H]
: