Commit 2024-05-27 20:43 46a17309

View on Github →

add pi-type AffineMaps (#10147) This adds AffineMap.pi, and some related extensionality lemmas.

Estimated changes

added theorem AffineMap.ext_linear
added def AffineMap.pi
added theorem AffineMap.pi_apply
added theorem AffineMap.pi_comp
added theorem AffineMap.pi_eq_zero
added theorem AffineMap.pi_ext_zero
added theorem AffineMap.pi_zero
added theorem AffineMap.proj_pi