Mathlib v3 is deprecated. Go to Mathlib v4

Theorem function.update_injective

Modification history

2020-10-30 14:20

src/logic/function/basic.lean

feat(algebra, logic): Pi instances for nontrivial and monoid_with_zero (#4766)

Added function.update_injective View on Github →