Commit 2025-01-16 07:44 0ec82d5a

View on Github →

feat: generalise PerfectPairing.restrictScalarsField (#20442) Also introduce the new definition PerfectPairing.IsPerfectCompl to simplify statements.

Estimated changes

Modified Mathlib/LinearAlgebra/PerfectPairing/Basic.lean

added structure PerfectPairing.IsPerfectCompl

added theorem PerfectPairing.mk_apply_apply

Modified Mathlib/LinearAlgebra/PerfectPairing/Restrict.lean

modified def PerfectPairing.restrict

modified def PerfectPairing.restrictScalarsField

added theorem PerfectPairing.restrictScalarsField_apply_apply

added theorem PerfectPairing.restrict_apply_apply

Modified Mathlib/LinearAlgebra/Span/Basic.lean

added theorem LinearMap.BilinMap.apply_apply_mem_of_mem_span

added def Submodule.inclusionSpan

added theorem Submodule.injective_inclusionSpan

modified theorem Submodule.span_le_restrictScalars

added theorem Submodule.span_range_inclusionSpan

added theorem Submodule.span_range_inclusion_eq_top

added theorem Submodule.span_range_inclusion_restrictScalars_eq_top

modified theorem Submodule.span_span_of_tower

modified theorem Submodule.span_subset_span

Modified Mathlib/LinearAlgebra/Span/Defs.lean

modified theorem Submodule.span_induction₂