Mathlib v3 is deprecated. Go to Mathlib v4

Def function.surjective.unique_of_surjective_const

Modification history

2022-03-04 21:44
src/logic/unique.lean
feat(ring_theory/simple_module): Simple modules as simple objects in the Module category (#11927) …
Added function.surjective.unique_of_surjective_constView on Github →