Mathlib v3 is deprecated. Go to Mathlib v4

Def unique_of_surjective_one

Modification history

2022-03-04 21:44

src/data/pi.lean

feat(ring_theory/simple_module): Simple modules as simple objects in the Module category (#11927) …

Added unique_of_surjective_one View on Github →