Commit 2023-09-16 14:32 2cd05f06

View on Github →

feat(LinearAlgebra/QuadraticForm/Basic): more lemmas (#7196) This also adds a handful of missing lemmas about Set.center for inverses and numeric literals.

Estimated changes

Modified Mathlib/GroupTheory/Subsemigroup/Center.lean

added theorem Set.intCast_mem_center

added theorem Set.invOf_mem_center

added theorem Set.natCast_mem_center

added theorem Set.ofNat_mem_center

added theorem Set.units_inv_mem_center

Modified Mathlib/LinearAlgebra/QuadraticForm/Basic.lean

added theorem BilinForm.polarBilin_toQuadraticForm

added theorem BilinForm.polar_toQuadraticForm

deleted theorem BilinForm.polar_to_quadratic_form

modified def LinearMap.compQuadraticForm

added theorem LinearMap.compQuadraticForm_polar

added theorem LinearMap.compQuadraticForm_polarBilin

modified def QuadraticForm.associatedHom

added theorem QuadraticForm.coe_associatedHom

added theorem QuadraticForm.two_nsmul_associated

Modified Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean

added theorem QuadraticForm.polarBilin_baseChange

added theorem QuadraticForm.polarBilin_tmul