Theorem OrzechProperty.bijective_of_surjective_of_injective

Modification history

2026-04-15 19:09
Mathlib/RingTheory/OrzechProperty.lean
feat(RingTheory/IsAdjoinRoot): add mkOfAdjoinEqTop' (#36421) …
Added OrzechProperty.bijective_of_surjective_of_injectiveView on Github →