Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-02-11 07:37 024aef0b

View on Github →

feat(data/pi): provide pi.mul_single (#11849) the additive version was previously called pi.single, to this requires refactoring existing code.

Estimated changes

added def one_hom.single
added theorem pi.mul_single_inv
added theorem pi.mul_single_mul
deleted theorem pi.single_add
added theorem pi.single_div
deleted theorem pi.single_neg
deleted theorem pi.single_sub
deleted def zero_hom.single
added theorem pi.apply_mul_single
added theorem pi.apply_mul_single₂
deleted theorem pi.apply_single
deleted theorem pi.apply_single₂
added def pi.mul_single
added theorem pi.mul_single_apply
added theorem pi.mul_single_comm
added theorem pi.mul_single_eq_of_ne
added theorem pi.mul_single_eq_same
added theorem pi.mul_single_inj
added theorem pi.mul_single_one
added theorem pi.mul_single_op
added theorem pi.mul_single_op₂
deleted def pi.single
deleted theorem pi.single_apply
deleted theorem pi.single_comm
deleted theorem pi.single_eq_of_ne'
deleted theorem pi.single_eq_of_ne
deleted theorem pi.single_eq_same
deleted theorem pi.single_inj
deleted theorem pi.single_injective
deleted theorem pi.single_op
deleted theorem pi.single_op₂
deleted theorem pi.single_zero
deleted theorem subsingleton.pi_single_eq