Theorem Basis.mulOpposite_apply

Modification history

2025-07-24 16:31

Mathlib/LinearAlgebra/Basis/MulOpposite.lean

chore: rename `Basis` to `Module.Basis` (#27381) …

Deleted Basis.mulOpposite_apply View on Github →

2025-07-23 11:19

Mathlib/LinearAlgebra/Basis/MulOpposite.lean

feat(LinearAlgebra/Basis/MulOpposite): basis of an opposite space (#25949) …

Added Basis.mulOpposite_apply View on Github →