mathlib
e605b21f - feat(linear_algebra/pi): add linear_equiv.Pi_congr_left (#8070)

Commit

4 years ago

feat(linear_algebra/pi): add linear_equiv.Pi_congr_left (#8070) This definition was hiding inside the proof for `is_noetherian_pi`

Author

eric-wieser

Parents