Commit 2024-03-18 23:55 346550b8

View on Github →

refactor(LinearAlgebra/BilinearForm/Basic): descope BilinForm to modules over commutative semirings (#11280) Require the module in the definition of the BilinForm structure to be over a commutative semiring. This PR is a per-requisite for #11278. It supersedes #10422. It's been pointed out elsewhere that the current definition over a non-commutative semiring doesn't make mathematical sense: https://github.com/leanprover-community/mathlib4/issues/10553#issuecomment-1944434170 Eventually the non-commutative situation may be considered in a mathematically meaningful way in the context of sesquilinear maps (e.g. something like https://github.com/leanprover-community/mathlib4/pull/9334#pullrequestreview-1880856848).

Estimated changes

modified def BilinForm.flipHom
modified def BilinForm.flipHomAux
modified theorem BilinForm.flip_apply
modified theorem BilinForm.flip_flip
modified theorem BilinForm.flip_flip_aux
modified structure BilinForm
modified theorem BilinForm.comp_congr
modified def BilinForm.congr
modified theorem BilinForm.congr_apply
modified theorem BilinForm.congr_comp
modified theorem BilinForm.congr_congr
modified theorem BilinForm.congr_refl
modified theorem BilinForm.congr_symm
modified theorem BilinForm.congr_trans
modified theorem BilinForm.ext_basis
modified def BilinForm.linMulLin
modified theorem BilinForm.linMulLin_comp
modified theorem BilinForm.toLin'Flip_apply
modified theorem BilinForm.toLin'_apply
modified def BilinForm.toLin
modified def BilinForm.toLinHom
modified theorem BilinForm.toLin_apply
modified def LinearMap.toBilin
modified def LinearMap.toBilinAux
modified theorem LinearMap.toBilinAux_eq
modified theorem LinearMap.toBilin_apply
modified theorem BilinForm.isSymm_iff_flip