Commit 2025-07-23 11:19 6d339610

View on Github →

feat(LinearAlgebra/Basis/MulOpposite): basis of an opposite space (#25949) This adds the definition of Basis.mulOpposite and shows finite-dimensionality and freeness of Hᵐᵒᵖ. For motivation, see #25951.

Estimated changes

Modified Mathlib.lean

Created Mathlib/LinearAlgebra/Basis/MulOpposite.lean

added theorem Basis.mulOpposite_apply

added theorem Basis.mulOpposite_repr_eq

added theorem Basis.mulOpposite_repr_op

added theorem Basis.repr_unop_eq_mulOpposite_repr

added theorem MulOpposite.finrank

added theorem MulOpposite.rank