Def Function.injective

Modification history

2022-10-24 23:24
Mathlib/Init/Function.lean
chore: capitalise Injective (#501) …
Deleted Function.injectiveView on Github →
2022-08-22 16:05
Mathlib/Init/Function.lean
fix: remove @[reducible] attribute from Function.injective (#375) …
Modified Function.injectiveView on Github →
2021-12-18 19:21
Mathlib/Init/Function.lean
feat: porting Data.List.Defs, Init.Data.List.Basic (#137) …
Modified Function.injectiveView on Github →
2021-06-09 11:55
Mathlib/Function.lean
feat (Data/Equiv/Basic): add `equiv` (#13) …
Added Function.injectiveView on Github →