Mathlib v3 is deprecated. Go to Mathlib v4

Theorem function.left_inverse.comp

Modification history

2020-08-31 08:47
src/logic/function/basic.lean
feat(measure_theory): induction principles in measure theory (#3978) …
Modified function.left_inverse.compView on Github →
2018-06-30 23:04
data/equiv/basic.lean
refactor(data/equiv): reorganize data.equiv deps
Modified function.left_inverse.compView on Github →
2017-12-11 14:09
data/equiv.lean
refactor(data/equiv): state refl, symm, and trans rules for equiv using projection. This gives more powerful rfl rules
Added function.left_inverse.compView on Github →