Commit 2024-04-12 08:07 66924a04

View on Github →

refactor(LinearAlgebra): replace Submodule.restrictBilinear by BilinForm.restrict (#12045) As discussed in this thread, there were 3 different definitions for the restriction of a bilinear form to a subspace. This PR deletes the definition Submodule.restrictBilinear, and replaces all its occurrences by the LinearMap.BilinForm.restrict one.

Estimated changes

Modified Mathlib/Algebra/Lie/Killing.lean

deleted theorem LieAlgebra.IsKilling.ker_restrictBilinear_eq_bot_of_isCartanSubalgebra

added theorem LieAlgebra.IsKilling.ker_restrict_eq_bot_of_isCartanSubalgebra

deleted theorem LieAlgebra.IsKilling.restrictBilinear_killingForm

added theorem LieAlgebra.IsKilling.restrict_killingForm

deleted theorem LieIdeal.restrictBilinear_killingForm

added theorem LieIdeal.restrict_killingForm

modified theorem LieModule.traceForm_flip

Modified Mathlib/Algebra/Module/Submodule/Bilinear.lean

deleted theorem LinearMap.ker_restrictBilinear_eq_of_codisjoint

Modified Mathlib/LinearAlgebra/BilinearForm/Basic.lean

Modified Mathlib/LinearAlgebra/BilinearForm/Orthogonal.lean

added theorem LinearMap.BilinForm.ker_restrict_eq_of_codisjoint

Modified Mathlib/LinearAlgebra/BilinearMap.lean