Theorem OrzechProperty.bijective_of_surjective_of_finrank_le

Modification history

2026-07-01 08:33
Mathlib/LinearAlgebra/Dimension/Free.lean
feat: simplify proof of `IsAdjoinRootMonic.mkOfAdjoinEqTop'` (#38189) …
Added OrzechProperty.bijective_of_surjective_of_finrank_leView on Github →