Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-10-30 14:20 bfadf057

View on Github →

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

Estimated changes

Modified src/algebra/group/pi.lean

deleted def pi.single

deleted theorem pi.single_eq_of_ne

deleted theorem pi.single_eq_same

Modified src/algebra/ring/pi.lean

Created src/data/pi.lean

added def pi.single

added theorem pi.single_eq_of_ne

added theorem pi.single_eq_same

added theorem pi.single_injective

Modified src/logic/function/basic.lean

added theorem function.update_injective

Modified src/logic/nontrivial.lean

added theorem pi.nontrivial_at