Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-02-17 11:38 ea1cff4a

View on Github →

feat(linear_algebra/pi): ext lemma for f : (Π i, M i) →ₗ[R] N (#6233)

Estimated changes

Modified src/algebra/big_operators/pi.lean

added theorem add_monoid_hom.functions_ext'

Modified src/linear_algebra/matrix.lean

Modified src/linear_algebra/std_basis.lean

added theorem linear_map.coe_std_basis

added theorem linear_map.pi_ext'

added theorem linear_map.pi_ext'_iff

added theorem linear_map.pi_ext

added theorem linear_map.pi_ext_iff