Commit 2024-04-16 19:49 e521a251

View on Github →

refactor(LinearAlgebra/BilinearForm/Basic): Derive the *_left and *_right results from the map_*₂ and map_* results (#12124) Following #11278 a number of the results in LinearAlgebra/BilinearForm/Basic are just special cases of results in LinearAlgebra/BilinearMap.

Estimated changes

Modified Mathlib/LinearAlgebra/BilinearForm/Basic.lean

modified theorem LinearMap.BilinForm.add_left

modified theorem LinearMap.BilinForm.congr_fun

modified theorem LinearMap.BilinForm.ext_iff

modified theorem LinearMap.BilinForm.neg_left

modified theorem LinearMap.BilinForm.neg_right

modified theorem LinearMap.BilinForm.smul_left

modified theorem LinearMap.BilinForm.sub_left

modified theorem LinearMap.BilinForm.sub_right

modified theorem LinearMap.BilinForm.zero_left

modified theorem LinearMap.BilinForm.zero_right