Commit 2023-06-04 14:19 e2b5ca37

View on Github →

style: allow _ for an argument in notation3 & replace _foo with _ in notation3 (#4652)

Estimated changes

modified theorem finprod_cond_eq_left
modified theorem finprod_cond_eq_right
modified theorem finprod_eq_if
modified theorem finprod_mem_mulSupport
modified theorem finprod_one
modified def Dfinsupp.toMultiset
modified def Multiset.toDfinsupp
modified def Dfinsupp.toFinsupp
modified theorem Dfinsupp.toFinsupp_add
modified theorem Dfinsupp.toFinsupp_coe
modified theorem Dfinsupp.toFinsupp_neg
modified theorem Dfinsupp.toFinsupp_sub
modified theorem Dfinsupp.toFinsupp_support
modified def Finsupp.toDfinsupp
modified theorem Real.ciInf_const_zero
modified theorem Real.ciSup_const_zero
modified theorem ENNReal.iSup_zero_eq_zero
modified theorem NNReal.iInf_const_zero
modified theorem Set.iInter_const
modified theorem Set.iInter_eq_if
modified theorem Set.iInter_univ
modified theorem Set.iUnion_const
modified theorem Set.iUnion_empty
modified theorem Set.iUnion_eq_if
modified theorem Set.iUnion_nonempty_self
modified theorem Set.sInter_eq_biInter
modified theorem Set.sUnion_eq_biUnion
modified theorem LinearMap.ker_smul'
modified theorem MeasureTheory.lintegral_one
modified theorem iInf_const
modified theorem iInf_const_mono
modified theorem iInf_eq_if
modified theorem iInf_le_iInf₂
modified theorem iInf_split_single
modified theorem iInf_subtype''
modified theorem iInf_top
modified theorem iSup_bot
modified theorem iSup_const
modified theorem iSup_const_le
modified theorem iSup_const_mono
modified theorem iSup_eq_if
modified theorem iSup_split_single
modified theorem iSup_subtype''
modified theorem iSup₂_le_iSup
modified theorem le_iInf_const
modified theorem ciInf_const
modified theorem ciSup_const
modified theorem Filter.HasBasis.eq_biInf
modified theorem Filter.HasBasis.sInter_sets
modified theorem Filter.eventually_const
modified theorem Filter.eventually_true
modified theorem Filter.frequently_const
modified theorem Filter.frequently_false
modified theorem Filter.const_eventuallyEq'
modified theorem Order.pred_eq_iSup
modified theorem Order.succ_eq_iInf
modified theorem tsum_zero'
modified theorem tsum_zero
modified theorem WithZeroTopology.nhds_zero
modified theorem nhds_def'
modified theorem Filter.nhds_nhds
modified theorem ENNReal.nhds_top
modified theorem ENNReal.nhds_zero
modified theorem ENNReal.tsum_iSup_eq
modified theorem EReal.nhds_bot
modified theorem EReal.nhds_top
modified theorem NNReal.nhds_zero
modified theorem Set.einfsep_insert_le