Commit 2024-07-20 07:03 2fc87a94

View on Github →

chore(*): use ⊕ notation for Sum (#14934)

Estimated changes

modified theorem Finset.prod_disj_sum
modified theorem Sum.smul_inl
modified theorem Sum.smul_inr
modified def CategoryTheory.Pi.sum
modified theorem CategoryTheory.sum_comp_inl
modified theorem CategoryTheory.sum_comp_inr
modified theorem Computable.sum_casesOn
modified theorem Partrec.fix
modified theorem Partrec.fix_aux
modified theorem Partrec.sum_casesOn_left
modified theorem Partrec.sum_casesOn_right
modified theorem Primrec.sum_casesOn
modified def Sum.bitraverse
modified theorem Finite.sum_left
modified theorem Finite.sum_right
modified theorem Finite.card_sum
modified def Finset.disjSum
modified theorem Finset.disjSum_mono_right
modified def Finsupp.sumElim
modified theorem Finsupp.sumElim_apply
modified theorem Fintype.prod_sum_type
modified def finSumEquivOfFinset
modified theorem infinite_sum
modified theorem Matrix.dotProduct_block
modified theorem Matrix.ext_iff_blocks
modified theorem Matrix.fromBlocks_toBlocks
modified def Matrix.toBlocks₁₁
modified def Matrix.toBlocks₁₂
modified def Matrix.toBlocks₂₁
modified def Matrix.toBlocks₂₂
modified def Multiset.disjSum
modified theorem PFun.dom_of_mem_fix
modified def PFun.fix
modified def PFun.fixInduction'
modified theorem PFun.fixInduction'_fwd
modified theorem PFun.fixInduction'_stop
modified def PFun.fixInduction
modified theorem PFun.fixInduction_spec
modified theorem PFun.fix_fwd
modified theorem PFun.fix_fwd_eq
modified theorem PFun.fix_stop
modified theorem PFun.mem_fix_iff
modified def PFunctor.M.corec'
modified def Computation.Bind.g
modified def Computation.BisimO
modified def Computation.Corec.f
modified def Computation.corec
modified theorem Computation.corec_eq
modified def Computation.destruct
modified def Computation.lmap
modified def Computation.rmap
modified theorem Set.compl_range_inl
modified theorem Set.compl_range_inr
modified theorem Set.preimage_inl_range_inr
modified theorem Set.preimage_inr_range_inl
modified theorem Sum.range_eq
modified theorem Sum.inl_injective
modified theorem Sum.inr_injective
modified theorem Sum.update_elim_inl
modified theorem Sum.update_elim_inr
modified theorem Sum.update_inl_apply_inl
modified theorem Sum.update_inl_apply_inr
modified theorem Sum.update_inl_comp_inl
modified theorem Sum.update_inl_comp_inr
modified theorem Sum.update_inr_apply_inl
modified theorem Sum.update_inr_apply_inr
modified theorem Sum.update_inr_comp_inl
modified theorem Sum.update_inr_comp_inr
modified def Sum3.in₀
modified def Sum3.in₁
modified def Sum3.in₂
modified def Finset.sumLexLift
modified def Finset.sumLift₂
modified theorem Sum.Icc_inl_inl
modified theorem Sum.Icc_inr_inr
modified theorem Sum.Ico_inl_inl
modified theorem Sum.Ico_inr_inr
modified theorem Sum.Ioc_inl_inl
modified theorem Sum.Ioc_inr_inr
modified theorem Sum.Ioo_inl_inl
modified theorem Sum.Ioo_inr_inr
modified def OrderIso.sumAssoc
modified def OrderIso.sumComm
modified theorem Sum.Lex.inl_bot
modified theorem Sum.Lex.inl_le_inl_iff
modified theorem Sum.Lex.inl_lt_inl_iff
modified theorem Sum.Lex.inr_le_inr_iff
modified theorem Sum.Lex.inr_top
modified theorem Sum.Lex.toLex_le_toLex
modified theorem Sum.Lex.toLex_lt_toLex
modified theorem Sum.Lex.toLex_mono
modified theorem Sum.Lex.toLex_strictMono
modified theorem Sum.inl_le_inl_iff
modified theorem Sum.inl_lt_inl_iff
modified theorem Sum.inl_mono
modified theorem Sum.inl_strictMono
modified theorem Sum.inr_le_inr_iff
modified theorem Sum.inr_lt_inr_iff
modified theorem Sum.inr_mono
modified theorem Sum.inr_strictMono
modified theorem Sum.le_def
modified theorem Sum.lt_def
modified theorem Sum.noMaxOrder_iff
modified theorem Sum.noMinOrder_iff
modified theorem Sum.swap_le_swap_iff
modified theorem Sum.swap_lt_swap_iff
modified theorem linearIndependent_sum
modified def Matrix.J
modified theorem SymplecticGroup.coe_inv'
modified theorem SymplecticGroup.mem_iff
modified def Encodable.decodeSum
modified theorem Encodable.decode_sum_val
modified def Encodable.encodeSum
modified theorem Encodable.encode_inl
modified theorem Encodable.encode_inr
modified theorem Equiv.Perm.sumCongr_apply
modified theorem Equiv.Perm.sumCongr_refl
modified def Equiv.emptySum
modified def Equiv.prodSumDistrib
modified def Equiv.psumCongr
modified def Equiv.psumEquivSum
modified def Equiv.sigmaNatSucc
modified def Equiv.sumAssoc
modified def Equiv.sumComm
modified def Equiv.sumCongr
modified theorem Equiv.sumCongr_refl
modified def Equiv.sumEmpty
modified def Equiv.sumProdDistrib
modified def finSumFinEquiv
modified theorem isEmpty_psum
modified theorem isEmpty_sum
modified theorem nonempty_psum
modified theorem nonempty_sum
modified theorem Dioph.ex_dioph
modified theorem iInf_sum
modified theorem iSup_sum
modified theorem Cardinal.add_def
modified theorem Cardinal.mk_psum
modified theorem Ordinal.lsub_sum
modified theorem Ordinal.sup_sum
modified theorem Sum.isConnected_iff
modified theorem Sum.isPreconnected_iff
modified def Homeomorph.sumCongr
modified theorem locallyFinite_sum
modified theorem Metric.Sum.dist_eq
modified def Metric.glueDist
modified theorem Metric.isometry_inl
modified theorem Metric.isometry_inr