Mathlib v3 is deprecated. Go to Mathlib v4

Theorem prod.mk.inj_iff

Modification history

2022-12-14 05:27
src/data/prod/basic.lean
feat(data/prod/basic): `prod.lex` is trichotomous (#17931) …
Modified prod.mk.inj_iffView on Github →
2017-12-06 13:30
data/prod.lean
feature(.): add various theorems
Modified prod.mk.inj_iffView on Github →
2017-09-03 20:55
logic/basic.lean
refactor(logic/basic): refactor logic theorems
Modified prod.mk.inj_iffView on Github →
2017-07-23 18:59
logic/basic.lean
refactor(*): attributes on same line
Modified prod.mk.inj_iffView on Github →
2017-07-23 18:29
logic/basic.lean
refactor(*): use 'lemma' iff statement is private
Modified prod.mk.inj_iffView on Github →
2017-07-23 15:16
logic/basic.lean
refactor(*): import content from lean/library/data and library_dev
Added prod.mk.inj_iffView on Github →