Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-04-05 17:46 26bf2730

View on Github →

feat(logic/embedding): embedding punit/prod (#2315)

feat(logic/embedding): embedding punit/prod
renaming to sectl
Revert disambiguations no longer needed

Estimated changes

Modified src/category_theory/products/basic.lean

deleted def category_theory.prod.inl

deleted def category_theory.prod.inr

added def category_theory.prod.sectl

added def category_theory.prod.sectr

modified theorem category_theory.prod_id_fst

modified theorem category_theory.prod_id_snd

Modified src/logic/embedding.lean

added theorem function.embedding.equiv_symm_to_embedding_trans_to_embedding

added theorem function.embedding.equiv_to_embedding_trans_symm_to_embedding

added def function.embedding.punit

added def function.embedding.sectl

added def function.embedding.sectr