Commit 2022-11-19 23:53 9964d231

View on Github →

chore: fixing some naming issues in Data/* (#570)

Estimated changes

Modified Mathlib/Data/Option/Basic.lean

added theorem Option.Mem.leftUnique

deleted theorem Option.Mem.left_unique

Modified Mathlib/Data/Prod/Basic.lean

Modified Mathlib/Data/Quot.lean

added theorem Quot.liftOn_mk

added theorem Quot.liftOn₂_mk

deleted theorem Quot.lift_on_mk

deleted theorem Quot.lift_on₂_mk

added theorem Quotient.hrecOn'_mk''

added theorem Quotient.hrecOn₂'_mk''

deleted theorem Quotient.hrec_on'_mk''

deleted theorem Quotient.hrec_on₂'_mk''

added theorem Quotient.liftOn_mk

added theorem Quotient.liftOn₂_mk

deleted theorem Quotient.lift_on_mk

deleted theorem Quotient.lift_on₂_mk

Modified Mathlib/Data/Sigma/Basic.lean

added theorem Prod.fst_comp_toSigma

deleted theorem Prod.fst_comp_to_sigma

added theorem Prod.fst_toSigma

deleted theorem Prod.fst_to_sigma

added theorem Prod.snd_toSigma

deleted theorem Prod.snd_to_sigma

added theorem Prod.toSigma_mk

deleted theorem Prod.to_sigma_mk