Commit 2024-10-21 09:29 662a8bae

View on Github →

chore(Data/NNReal): split into Defs and Basic (#17913) I saw a few weird imports in Data.NNReal.Basic so I decided to split off a Defs file. Defs conains the definition and the conditionally complete linear ordered archimedean commutative semifield(!) structure, and all easily definable lemmas downstream of that. Basic contains whatever was left over and is a good target for further cleanup and reorganization.

Estimated changes

deleted theorem NNReal.abs_eq
deleted theorem NNReal.algebraMap_eq_coe
deleted theorem NNReal.bddAbove_coe
deleted theorem NNReal.bddBelow_coe
deleted theorem NNReal.bot_eq_zero
deleted theorem NNReal.coe_eq_one
deleted theorem NNReal.coe_eq_zero
deleted theorem NNReal.coe_iInf
deleted theorem NNReal.coe_iSup
deleted theorem NNReal.coe_image
deleted theorem NNReal.coe_inj
deleted theorem NNReal.coe_le_coe
deleted theorem NNReal.coe_le_one
deleted theorem NNReal.coe_lt_coe
deleted theorem NNReal.coe_lt_one
deleted theorem NNReal.coe_max
deleted theorem NNReal.coe_min
deleted theorem NNReal.coe_mk
deleted theorem NNReal.coe_mono
deleted theorem NNReal.coe_ne_one
deleted theorem NNReal.coe_ne_zero
deleted theorem NNReal.coe_nnqsmul
deleted theorem NNReal.coe_nonneg
deleted theorem NNReal.coe_nsmul
deleted theorem NNReal.coe_one
deleted theorem NNReal.coe_pos
deleted theorem NNReal.coe_pow
deleted theorem NNReal.coe_sInf
deleted theorem NNReal.coe_sSup
deleted theorem NNReal.coe_sub_def
deleted theorem NNReal.coe_toRealHom
deleted theorem NNReal.coe_zero
deleted theorem NNReal.coe_zpow
deleted theorem NNReal.div_le_of_le_mul'
deleted theorem NNReal.div_le_of_le_mul
deleted theorem NNReal.div_lt_iff'
deleted theorem NNReal.div_lt_iff
deleted theorem NNReal.div_lt_one_of_lt
deleted theorem NNReal.iInf_const_zero
deleted theorem NNReal.iInf_empty
deleted theorem NNReal.iSup_empty
deleted theorem NNReal.iSup_eq_zero
deleted theorem NNReal.inv_le
deleted theorem NNReal.inv_le_of_le_mul
deleted theorem NNReal.inv_lt_inv
deleted theorem NNReal.inv_lt_one_iff
deleted theorem NNReal.le_div_iff'
deleted theorem NNReal.le_div_iff_mul_le
deleted theorem NNReal.le_inv_iff_mul_le
deleted theorem NNReal.lt_div_iff'
deleted theorem NNReal.lt_div_iff
deleted theorem NNReal.lt_inv_iff_mul_lt
deleted theorem NNReal.mk_natCast
deleted theorem NNReal.mk_one
deleted theorem NNReal.mk_zero
deleted theorem NNReal.mul_eq_mul_left
deleted theorem NNReal.mul_le_iff_le_inv
deleted theorem NNReal.mul_lt_of_lt_div
deleted theorem NNReal.mul_sup
deleted theorem NNReal.ne_iff
deleted theorem NNReal.one_le_coe
deleted theorem NNReal.one_lt_coe
deleted theorem NNReal.pow_antitone_exp
deleted theorem NNReal.sInf_empty
deleted theorem NNReal.smul_def
deleted theorem NNReal.sub_def
deleted theorem NNReal.sup_mul
deleted theorem NNReal.toNNReal_coe_nat
deleted def NNReal.toReal
deleted def NNReal.toRealHom
deleted theorem NNReal.val_eq_coe
deleted theorem NNReal.zero_le_coe
deleted def NNReal
deleted theorem Real.coe_nnabs
deleted theorem Real.coe_toNNReal'
deleted theorem Real.coe_toNNReal
deleted theorem Real.coe_toNNReal_le
deleted theorem Real.le_coe_toNNReal
deleted theorem Real.lt_of_toNNReal_lt
deleted theorem Real.natCast_le_toNNReal
deleted theorem Real.natCast_lt_toNNReal
deleted theorem Real.natCastle_toNNReal'
deleted def Real.nnabs
deleted theorem Real.nnabs_coe
deleted theorem Real.nnabs_of_nonneg
deleted theorem Real.ofNat_le_toNNReal
deleted theorem Real.ofNat_lt_toNNReal
deleted theorem Real.one_le_toNNReal
deleted theorem Real.one_lt_toNNReal
deleted theorem Real.toNNReal_abs
deleted theorem Real.toNNReal_add
deleted theorem Real.toNNReal_add_le
deleted theorem Real.toNNReal_coe
deleted theorem Real.toNNReal_div'
deleted theorem Real.toNNReal_div
deleted theorem Real.toNNReal_eq_natCast
deleted theorem Real.toNNReal_eq_ofNat
deleted theorem Real.toNNReal_eq_one
deleted theorem Real.toNNReal_eq_zero
deleted theorem Real.toNNReal_inv
deleted theorem Real.toNNReal_le_natCast
deleted theorem Real.toNNReal_le_ofNat
deleted theorem Real.toNNReal_le_one
deleted theorem Real.toNNReal_le_toNNReal
deleted theorem Real.toNNReal_lt_natCast'
deleted theorem Real.toNNReal_lt_natCast
deleted theorem Real.toNNReal_lt_ofNat
deleted theorem Real.toNNReal_lt_one
deleted theorem Real.toNNReal_mul
deleted theorem Real.toNNReal_ofNat
deleted theorem Real.toNNReal_of_nonneg
deleted theorem Real.toNNReal_of_nonpos
deleted theorem Real.toNNReal_one
deleted theorem Real.toNNReal_pos
deleted theorem Real.toNNReal_pow
deleted theorem Real.toNNReal_zero
added theorem NNReal.abs_eq
added theorem NNReal.bddAbove_coe
added theorem NNReal.bddBelow_coe
added theorem NNReal.bot_eq_zero
added theorem NNReal.coe_eq_one
added theorem NNReal.coe_eq_zero
added theorem NNReal.coe_iInf
added theorem NNReal.coe_iSup
added theorem NNReal.coe_image
added theorem NNReal.coe_inj
added theorem NNReal.coe_le_coe
added theorem NNReal.coe_le_one
added theorem NNReal.coe_lt_coe
added theorem NNReal.coe_lt_one
added theorem NNReal.coe_max
added theorem NNReal.coe_min
added theorem NNReal.coe_mk
added theorem NNReal.coe_mono
added theorem NNReal.coe_ne_one
added theorem NNReal.coe_ne_zero
added theorem NNReal.coe_nnqsmul
added theorem NNReal.coe_nonneg
added theorem NNReal.coe_nsmul
added theorem NNReal.coe_one
added theorem NNReal.coe_pos
added theorem NNReal.coe_pow
added theorem NNReal.coe_sInf
added theorem NNReal.coe_sSup
added theorem NNReal.coe_sub_def
added theorem NNReal.coe_toRealHom
added theorem NNReal.coe_zero
added theorem NNReal.coe_zpow
added theorem NNReal.div_lt_iff'
added theorem NNReal.div_lt_iff
added theorem NNReal.iInf_const_zero
added theorem NNReal.iInf_empty
added theorem NNReal.iSup_empty
added theorem NNReal.iSup_eq_zero
added theorem NNReal.inv_le
added theorem NNReal.inv_lt_inv
added theorem NNReal.inv_lt_one_iff
added theorem NNReal.le_div_iff'
added theorem NNReal.lt_div_iff'
added theorem NNReal.lt_div_iff
added theorem NNReal.mk_natCast
added theorem NNReal.mk_one
added theorem NNReal.mk_zero
added theorem NNReal.mul_eq_mul_left
added theorem NNReal.mul_sup
added theorem NNReal.ne_iff
added theorem NNReal.one_le_coe
added theorem NNReal.one_lt_coe
added theorem NNReal.sInf_empty
added theorem NNReal.smul_def
added theorem NNReal.sub_def
added theorem NNReal.sup_mul
added def NNReal.toReal
added def NNReal.toRealHom
added theorem NNReal.val_eq_coe
added theorem NNReal.zero_le_coe
added def NNReal
added theorem Real.coe_nnabs
added theorem Real.coe_toNNReal'
added theorem Real.coe_toNNReal
added theorem Real.coe_toNNReal_le
added theorem Real.le_coe_toNNReal
added theorem Real.lt_of_toNNReal_lt
added def Real.nnabs
added theorem Real.nnabs_coe
added theorem Real.nnabs_of_nonneg
added theorem Real.ofNat_le_toNNReal
added theorem Real.ofNat_lt_toNNReal
added theorem Real.one_le_toNNReal
added theorem Real.one_lt_toNNReal
added theorem Real.toNNReal_abs
added theorem Real.toNNReal_add
added theorem Real.toNNReal_add_le
added theorem Real.toNNReal_coe
added theorem Real.toNNReal_div'
added theorem Real.toNNReal_div
added theorem Real.toNNReal_eq_ofNat
added theorem Real.toNNReal_eq_one
added theorem Real.toNNReal_eq_zero
added theorem Real.toNNReal_inv
added theorem Real.toNNReal_le_ofNat
added theorem Real.toNNReal_le_one
added theorem Real.toNNReal_lt_ofNat
added theorem Real.toNNReal_lt_one
added theorem Real.toNNReal_mul
added theorem Real.toNNReal_ofNat
added theorem Real.toNNReal_one
added theorem Real.toNNReal_pos
added theorem Real.toNNReal_pow
added theorem Real.toNNReal_zero