Commit 2022-11-28 15:54 c2db4e5c

View on Github →

feat: port Data.Pi.Algebra (#564)

  • depends on: #579 Mathlib SHA: 17a9f8f7a4ef32ee65d418103367cf30e84e631d Done with the reviews. This should hopefully now be ready to merge.

Estimated changes

added theorem Function.extend_div
added theorem Function.extend_inv
added theorem Function.extend_mul
added theorem Function.extend_one
added theorem Pi.apply_mulSingle
added theorem Pi.apply_mulSingle₂
added theorem Pi.bit0_apply
added theorem Pi.bit1_apply
added theorem Pi.comp_one
added theorem Pi.const_div
added theorem Pi.const_inv
added theorem Pi.const_mul
added theorem Pi.const_one
added theorem Pi.const_pow
added theorem Pi.div_apply
added theorem Pi.div_comp
added theorem Pi.div_def
added theorem Pi.inv_apply
added theorem Pi.inv_comp
added theorem Pi.inv_def
added def Pi.mulSingle
added theorem Pi.mulSingle_apply
added theorem Pi.mulSingle_comm
added theorem Pi.mulSingle_eq_of_ne'
added theorem Pi.mulSingle_eq_of_ne
added theorem Pi.mulSingle_eq_same
added theorem Pi.mulSingle_inj
added theorem Pi.mulSingle_injective
added theorem Pi.mulSingle_one
added theorem Pi.mulSingle_op
added theorem Pi.mulSingle_op₂
added theorem Pi.mul_apply
added theorem Pi.mul_comp
added theorem Pi.mul_def
added theorem Pi.one_apply
added theorem Pi.one_comp
added theorem Pi.one_def
added theorem Pi.pow_apply
added theorem Pi.pow_comp
added theorem Pi.pow_def
added theorem Pi.prod_fst_snd
added theorem Pi.prod_snd_fst
added theorem Pi.smul_apply
added theorem Pi.smul_comp
added theorem Pi.smul_const
added theorem Pi.smul_def
added theorem Sum.elim_div_div
added theorem Sum.elim_inv_inv
added theorem Sum.elim_mulSingle_one
added theorem Sum.elim_mul_mul
added theorem Sum.elim_one_mulSingle
added theorem Sum.elim_one_one