Commit 2026-07-01 08:33 b4b33fa6

View on Github →

feat: simplify proof of IsAdjoinRootMonic.mkOfAdjoinEqTop' (#38189)

Simplify the proof of IsAdjoinRootMonic.mkOfAdjoinEqTop' by factoring out a lemma OrzechProperty.bijective_of_surjective_of_finrank_le and making use of the existing lemma finrank_le_iff_exists_linearMap.

Estimated changes

Modified Mathlib/LinearAlgebra/Dimension/Free.lean

added theorem OrzechProperty.bijective_of_surjective_of_finrank_le

Modified Mathlib/RingTheory/IsAdjoinRoot.lean

modified def IsAdjoinRootMonic.mkOfAdjoinEqTop'