WithTop

📁 Source: Mathlib/Algebra/Order/Monoid/Unbundled/WithTop.lean

Statistics

Metric	Count
Definitions `withBotMap`, `withTopMap`, `withBotMap`, `withTopMap`, `withBotMap`, `withTopMap`, `AddSemigroup`, `add`, `addCommMonoid`, `addCommMonoidWithOne`, `addCommSemigroup`, `addHom`, `addMonoid`, `addMonoidWithOne`, `addZeroClass`, `one`, `zero`, `add`, `addCommMonoid`, `addCommMonoidWithOne`, `addCommSemigroup`, `addHom`, `addMonoid`, `addMonoidWithOne`, `addSemigroup`, `addZeroClass`, `one`, `zero`, `withBotMap`, `withTopMap`	30
Theorems `withBotMap_apply`, `withTopMap_apply`, `withBotMap_apply`, `withTopMap_apply`, `withBotMap_apply`, `withTopMap_apply`, `addLECancellable_coe`, `addLECancellable_iff_ne_bot`, `addLECancellable_of_lt_bot`, `addLECancellable_of_ne_bot`, `addLeftMono`, `addLeftReflectLT`, `addRightMono`, `addRightReflectLT`, `add_bot`, `add_coe_eq_bot_iff`, `add_eq_bot`, `add_eq_coe`, `add_le_add_iff_left`, `add_le_add_iff_right`, `add_le_add_iff_right'`, `add_left_cancel`, `add_left_inj`, `add_lt_add_iff_left`, `add_lt_add_iff_right`, `add_lt_add_left`, `add_lt_add_of_le_of_lt`, `add_lt_add_of_lt_of_le`, `add_lt_add_right`, `add_ne_bot`, `add_right_cancel`, `add_right_inj`, `bot_add`, `bot_lt_add`, `bot_lt_natCast`, `bot_lt_one`, `bot_ne_natCast`, `bot_ne_ofNat`, `bot_ne_one`, `bot_ne_zero`, `bot_neg`, `charZero`, `coe_add`, `coe_addHom`, `coe_add_eq_bot_iff`, `coe_eq_ofNat`, `coe_eq_one`, `coe_eq_zero`, `coe_le_one`, `coe_le_zero`, `coe_lt_one`, `coe_lt_zero`, `coe_natCast`, `coe_nonneg`, `coe_nsmul`, `coe_ofNat`, `coe_one`, `coe_pos`, `coe_zero`, `le_of_add_le_add_left`, `le_of_add_le_add_right`, `map_add`, `map_eq_natCast_iff`, `map_eq_ofNat_iff`, `map_eq_one_iff`, `map_eq_zero_iff`, `map_natCast`, `map_ofNat`, `map_one`, `map_zero`, `natCast_eq_map_iff`, `natCast_ne_bot`, `ofNat_eq_coe`, `ofNat_eq_map_iff`, `ofNat_ne_bot`, `one_eq_coe`, `one_eq_map_iff`, `one_le_coe`, `one_lt_coe`, `one_ne_bot`, `unbotD_one`, `unbotD_zero`, `unbot_one`, `unbot_zero`, `zeroLEOneClass`, `zero_eq_coe`, `zero_eq_map_iff`, `zero_ne_bot`, `addLECancellable_coe`, `addLECancellable_iff_ne_top`, `addLECancellable_of_lt_top`, `addLECancellable_of_ne_top`, `addLeftMono`, `addLeftReflectLT`, `addRightMono`, `addRightReflectLT`, `add_coe_eq_top_iff`, `add_eq_coe`, `add_eq_top`, `add_le_add_iff_left`, `add_le_add_iff_right`, `add_left_cancel`, `add_left_inj`, `add_lt_add`, `add_lt_add_iff_left`, `add_lt_add_iff_right`, `add_lt_add_left`, `add_lt_add_of_le_of_lt`, `add_lt_add_of_lt_of_le`, `add_lt_add_right`, `add_lt_top`, `add_ne_top`, `add_right_cancel`, `add_right_inj`, `add_top`, `charZero`, `coe_add`, `coe_addHom`, `coe_add_eq_top_iff`, `coe_eq_ofNat`, `coe_eq_one`, `coe_eq_zero`, `coe_le_one`, `coe_le_zero`, `coe_lt_one`, `coe_lt_zero`, `coe_natCast`, `coe_ne_one`, `coe_ne_zero`, `coe_nonneg`, `coe_nsmul`, `coe_ofNat`, `coe_one`, `coe_pos`, `coe_zero`, `existsAddOfLE`, `le_of_add_le_add_left`, `le_of_add_le_add_right`, `map_add`, `map_eq_natCast_iff`, `map_eq_ofNat_iff`, `map_eq_one_iff`, `map_eq_zero_iff`, `map_natCast`, `map_ofNat`, `map_one`, `map_zero`, `natCast_eq_map_iff`, `natCast_lt_top`, `natCast_ne_top`, `ofNat_eq_coe`, `ofNat_eq_map_iff`, `ofNat_ne_top`, `one_eq_coe`, `one_eq_map_iff`, `one_le_coe`, `one_lt_coe`, `one_lt_top`, `one_ne_top`, `top_add`, `top_ne_natCast`, `top_ne_ofNat`, `top_ne_one`, `top_ne_zero`, `top_pos`, `untopD_one`, `untopD_zero`, `untop_one`, `untop_zero`, `zeroLEOneClass`, `zero_eq_coe`, `zero_eq_map_iff`, `zero_ne_top`, `withBotMap_apply`, `withTopMap_apply`	175
Total	205

AddHom

Definitions

Name	Category	Theorems
`withBotMap` 📖	CompOp	1 math math: `withBotMap_apply`
`withTopMap` 📖	CompOp	1 math math: `withTopMap_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`withBotMap_apply` 📖	mathematical	—	`DFunLike.coe` `AddHom` `WithBot` `WithBot.add` `funLike` `withBotMap` `WithBot.map`	—	—
`withTopMap_apply` 📖	mathematical	—	`DFunLike.coe` `AddHom` `WithTop` `WithTop.add` `funLike` `withTopMap` `WithTop.map`	—	—

AddMonoidHom

Definitions

Name	Category	Theorems
`withBotMap` 📖	CompOp	1 math math: `withBotMap_apply`
`withTopMap` 📖	CompOp	1 math math: `withTopMap_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`withBotMap_apply` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `WithBot` `AddZeroClass.toAddZero` `WithBot.addZeroClass` `instFunLike` `withBotMap` `WithBot.map`	—	—
`withTopMap_apply` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `WithTop` `AddZeroClass.toAddZero` `WithTop.addZeroClass` `instFunLike` `withTopMap` `WithTop.map`	—	—

OneHom

Definitions

Name	Category	Theorems
`withBotMap` 📖	CompOp	1 math math: `withBotMap_apply`
`withTopMap` 📖	CompOp	1 math math: `withTopMap_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`withBotMap_apply` 📖	mathematical	—	`DFunLike.coe` `OneHom` `WithBot` `WithBot.one` `funLike` `withBotMap` `WithBot.map`	—	—
`withTopMap_apply` 📖	mathematical	—	`DFunLike.coe` `OneHom` `WithTop` `WithTop.one` `funLike` `withTopMap` `WithTop.map`	—	—

WithBot

Definitions

Name	Category	Theorems
`AddSemigroup` 📖	CompOp	—
`add` 📖	CompOp	97 math math: `add_le_add_iff_right'`, `Polynomial.degree_mul_le`, `Polynomial.degree_add_div`, `ringKrullDim_quotient_span_singleton_succ_eq_ringKrullDim`, `ringKrullDim_succ_le_ringKrullDim_polynomial`, `addRightMono`, `addLeftMono`, `Module.supportDim_add_length_eq_supportDim_of_isRegular`, `Nat.WithBot.add_eq_two_iff`, `Polynomial.degree_list_prod`, `lt_add_one_iff`, `Polynomial.degree_list_prod_le`, `ringKrullDim_quotSMulTop_succ_eq_ringKrullDim_of_mem_jacobson`, `add_le_add_iff_left`, `ringKrullDim_succ_le_ringKrullDim_powerseries`, `addLeftReflectLT`, `add_coe_eq_bot_iff`, `ringKrullDim_quotSMulTop_succ_eq_ringKrullDim`, `addLECancellable_of_ne_bot`, `Order.krullDim_le_of_krullDim_preimage_le`, `bot_add`, `Polynomial.degree_mul_le_of_le`, `Module.supportDim_quotSMulTop_succ_eq_of_notMem_minimalPrimes_of_mem_maximalIdeal`, `ringKrullDim_succ_le_of_surjective`, `Finset.fold_max_add`, `add_bot`, `Nat.WithBot.add_eq_one_iff`, `add_le_add_iff_right`, `WeierstrassCurve.Affine.CoordinateRing.degree_norm_smul_basis`, `WithZero.toMulBot_lt`, `bot_lt_add`, `Module.ringKrullDim_quotient_add_one_of_mem_nonZeroDivisors`, `Order.krullDim_WithTop`, `ringKrullDim_le_ringKrullDim_quotient_add_card`, `Nat.WithBot.add_eq_three_iff`, `Ideal.height_le_ringKrullDim_quotient_add_one`, `addLECancellable_coe`, `ringKrullDim_le_ringKrullDim_quotient_add_spanFinrank`, `add_lt_add_of_lt_of_le`, `add_lt_add_left`, `WithZero.toMulBot_coe_ofAdd`, `add_eq_coe`, `map_add`, `ringKrullDim_add_length_eq_ringKrullDim_of_isRegular`, `Ideal.height_le_ringKrullDim_quotient_add_encard`, `Polynomial.degree_wronskian_lt_add`, `ringKrullDim_quotient_span_singleton_succ_eq_ringKrullDim_of_mem_nonZeroDivisors`, `coe_add_eq_bot_iff`, `Module.supportDim_quotSMulTop_succ_eq_supportDim`, `Polynomial.degree_mul'`, `ringKrullDim_quotient_succ_le_of_nonZeroDivisor`, `ringKrullDim_quotient_span_singleton_succ_eq_ringKrullDim_of_mem_jacobson`, `WithZero.toMulBot_zero`, `ringKrullDim_add_natCard_le_ringKrullDim_mvPolynomial`, `addLECancellable_of_lt_bot`, `ringKrullDim_le_ringKrullDim_add_card`, `Module.supportDim_le_supportDim_quotSMulTop_succ`, `addLECancellable_iff_ne_bot`, `Module.supportDim_quotSMulTop_succ_eq_supportDim_mem_jacobson`, `Polynomial.Monic.degree_mul`, `Polynomial.ringKrullDim_le`, `WithZero.toMulBot_coe`, `Polynomial.degree_add_degree_leadingCoeff_inv`, `Polynomial.degree_add_divByMonic`, `Order.krullDim_withBot`, `le_add_self`, `Module.supportDim_le_supportDim_quotSMulTop_succ_of_mem_jacobson`, `Nat.WithBot.add_one_le_of_lt`, `Polynomial.degree_mul_X`, `height_le_ringKrullDim_quotient_add_spanFinrank`, `Nat.WithBot.add_eq_zero_iff`, `ringKrullDim_add_enatCard_le_ringKrullDim_mvPolynomial`, `add_right_inj`, `ringKrullDim_le_ringKrullDim_add_spanFinrank`, `le_self_add`, `add_lt_add_right`, `coe_add`, `WithZero.toMulBot_le`, `addRightReflectLT`, `Polynomial.ringKrullDim_of_isNoetherianRing`, `add_lt_add_of_le_of_lt`, `MvPolynomial.ringKrullDim_of_isNoetherianRing`, `Module.supportDim_quotSMulTop_succ_eq_of_notMem_minimalPrimes_of_mem_jacobson`, `Polynomial.degree_mul_X_pow`, `ringKrullDim_le_ringKrullDim_quotSMulTop_succ`, `Module.supportDim_quotSMulTop_succ_le_of_notMem_minimalPrimes`, `AddHom.withBotMap_apply`, `WithZero.toMulBot_symm_bot`, `add_left_inj`, `add_lt_add_iff_left`, `Order.krullDim_le_of_krullDim_preimage_le'`, `WithZero.toMulBot_strictMono`, `ringKrullDim_le_ringKrullDim_quotient_add_encard`, `Polynomial.degree_mul`, `add_lt_add_iff_right`, `add_eq_bot`, `add_one_le_iff`
`addCommMonoid` 📖	CompOp	12 math math: `sum_eq_bot_iff`, `Polynomial.degree_multiset_prod_of_monic`, `Polynomial.degree_prod_le`, `Polynomial.degree_prod`, `Polynomial.degree_multiset_prod_le`, `Polynomial.degree_prod_of_monic`, `isOrderedAddMonoid`, `instArchimedean`, `sum_lt_bot`, `bot_lt_sum_iff`, `coe_sum`, `Polynomial.degree_multiset_prod`
`addCommMonoidWithOne` 📖	CompOp	—
`addCommSemigroup` 📖	CompOp	—
`addHom` 📖	CompOp	1 math math: `coe_addHom`
`addMonoid` 📖	CompOp	5 math math: `Polynomial.degree_pow_le`, `Polynomial.degree_pow`, `WeierstrassCurve.Affine.CoordinateRing.degree_norm_smul_basis`, `coe_nsmul`, `Polynomial.degree_pow'`
`addMonoidWithOne` 📖	CompOp	136 math math: `WittVector.RecursionMain.succNthDefiningPoly_degree`, `Polynomial.degree_pow_le_of_le`, `Order.LTSeries.length_le_krullDim`, `Order.krullDim_lt_coe_iff`, `Polynomial.coe_lt_degree`, `Polynomial.MonicDegreeEq.degree`, `CategoryTheory.injectiveDimension_le_iff`, `Polynomial.degree_quadratic_lt`, `map_eq_natCast_iff`, `Ring.krullDimLE_iff`, `Polynomial.Sequence.degree_eq'`, `PowerSeries.degree_weierstrassMod_lt`, `Polynomial.degree_eq_natDegree`, `Module.supportDim_add_length_eq_supportDim_of_isRegular`, `Nat.WithBot.add_eq_two_iff`, `Order.le_krullDim_iff`, `lt_add_one_iff`, `Polynomial.IsDistinguishedAt.degree_eq_coe_lift_order_map`, `Lagrange.eq_interpolate_iff`, `Polynomial.degree_X_pow_add_C`, `PowerSeries.degree_trunc_lt`, `Polynomial.card_roots_map_le_degree`, `Cubic.degree_of_a_eq_zero'`, `MvPolynomial.degree_optionEquivLeft`, `Polynomial.Splits.degree_eq_card_roots`, `Cubic.degree_of_a_ne_zero'`, `Polynomial.degree_quadratic`, `minpoly.degree_le`, `PowerSeries.IsWeierstrassDivisionAt.degree_lt`, `Polynomial.degree_cubic_lt`, `Matrix.charpoly_degree_eq_dim`, `CategoryTheory.injectiveDimension_ge_iff`, `Polynomial.Chebyshev.degree_T`, `Polynomial.degree_X_pow_le`, `Polynomial.degree_monomial_le`, `Polynomial.natDegree_lt_iff_degree_lt`, `Lagrange.degree_interpolate_erase_lt`, `Polynomial.degree_quadratic_le`, `CategoryTheory.projectiveDimension_lt_iff`, `Lagrange.degree_interpolate_lt`, `map_natCast`, `Polynomial.Sequence.degree_eq`, `Polynomial.exists_approx_polynomial_aux`, `Polynomial.degree_freeMonic`, `PowerBasis.mem_span_pow'`, `WeierstrassCurve.Affine.CoordinateRing.degree_norm_smul_basis`, `Polynomial.degree_derivative_eq`, `Polynomial.degree_le_of_natDegree_le`, `ringKrullDim_le_ringKrullDim_quotient_add_card`, `Nat.WithBot.add_eq_three_iff`, `PowerBasis.degree_minpoly`, `Polynomial.degree_hermite`, `Lagrange.degree_nodal`, `Polynomial.degree_X_pow_sub_C`, `Polynomial.degree_le_natDegree`, `natCast_eq_map_iff`, `ringKrullDim_le_ringKrullDim_quotient_add_spanFinrank`, `Polynomial.exists_multiset_roots`, `Ideal.mem_leadingCoeffNth`, `bot_lt_natCast`, `Polynomial.degree_C_mul_X_pow_le`, `charZero`, `Polynomial.Chebyshev.degree_U_of_ne_neg_one`, `ringKrullDim_add_length_eq_ringKrullDim_of_isRegular`, `Polynomial.degreeLT_succ_eq_degreeLE`, `Polynomial.degree_eq_iff_natDegree_eq_of_pos`, `Ideal.is_fg_degreeLE`, `Polynomial.degree_cubic`, `Cubic.degree_of_a_eq_zero`, `Polynomial.degree_X_pow`, `Cubic.equiv_symm_apply_b`, `Lagrange.degree_basis`, `ringKrullDim_add_natCard_le_ringKrullDim_mvPolynomial`, `WeierstrassCurve.Affine.degree_polynomial`, `LinearRecurrence.charPoly_degree_eq_order`, `ringKrullDim_le_ringKrullDim_add_card`, `Lagrange.degree_interpolate_le`, `CategoryTheory.projectiveDimension_le_iff`, `Cubic.degree_of_a_ne_zero`, `MvPolynomial.degree_finSuccEquiv`, `CategoryTheory.projectiveDimension_ge_iff`, `Field.primitive_element_iff_minpoly_degree_eq`, `CategoryTheory.injectiveDimension_lt_iff`, `Polynomial.ringKrullDim_le`, `Matrix.charpoly_sub_diagonal_degree_lt`, `Cubic.equiv_symm_apply_c`, `Polynomial.card_roots`, `Polynomial.ofFn_degree_lt`, `Polynomial.degree_eq_card_roots`, `PowerBasis.degree_minpolyGen`, `succ_natCast`, `ringKrullDim_nat`, `Polynomial.degree_lt_iff_coeff_zero`, `Nat.cast_withBot`, `Polynomial.degree_cyclotomic'`, `Polynomial.le_degree_of_ne_zero`, `Cubic.equiv_apply_coe`, `PowerSeries.IsWeierstrassFactorization.degree_eq_coe_lift_order_map`, `Polynomial.le_degree_of_mem_supp`, `height_le_ringKrullDim_quotient_add_spanFinrank`, `PowerSeries.IsWeierstrassFactorizationAt.degree_eq_coe_lift_order_map_of_ne_top`, `PowerSeries.isWeierstrassDivisionAt_iff`, `Polynomial.degree_update_le`, `Polynomial.integralNormalization_coeff`, `Cubic.degree_of_b_ne_zero'`, `Polynomial.degree_shiftedLegendre`, `Order.krullDim_eq_length_of_finiteDimensionalOrder`, `Polynomial.span_le_degreeLE_of_finite`, `Order.KrullDimLE.krullDim_le`, `ringKrullDim_le_ringKrullDim_add_spanFinrank`, `Polynomial.degree_cubic_le`, `Cubic.equiv_symm_apply_d`, `Irreducible.degree_le_two`, `Polynomial.degree_eq_card_roots'`, `Cubic.equiv_symm_apply_a`, `MvPolynomial.ringKrullDim_of_isNoetherianRing`, `Polynomial.degree_sum_fin_lt`, `Polynomial.degree_eq_iff_natDegree_eq`, `Polynomial.degreeLE_eq_span_X_pow`, `Polynomial.natDegree_le_iff_degree_le`, `Polynomial.degree_monomial`, `Polynomial.degree_mul_X_pow`, `Nat.WithBot.coe_nonneg`, `Polynomial.degree_C_mul_X_pow`, `coe_natCast`, `Polynomial.Chebyshev.degree_U_natCast`, `Polynomial.degree_cyclotomic`, `Polynomial.card_roots_sub_C`, `Polynomial.mem_degreeLT`, `PowerBasis.dim_le_degree_of_root`, `Polynomial.degree_linear_lt`, `Order.krullDimLE_iff`, `Polynomial.exists_mul_add_mul_eq_C_resultant`, `Cubic.degree_of_b_ne_zero`, `Polynomial.roots_def`, `add_one_le_iff`
`addZeroClass` 📖	CompOp	2 math math: `coe_addHom`, `AddMonoidHom.withBotMap_apply`
`one` 📖	CompOp	93 math math: `coe_eq_one`, `ringKrullDim_quotient_span_singleton_succ_eq_ringKrullDim`, `ringKrullDim_succ_le_ringKrullDim_polynomial`, `zeroLEOneClass`, `coe_lt_one`, `Cubic.degree_of_b_eq_zero`, `map_eq_one_iff`, `ringKrullDim_eq_one_iff_of_isLocalRing_isDomain`, `Order.krullDim_le_one_iff`, `Nat.WithBot.add_eq_two_iff`, `Polynomial.Splits.degree_le_one_of_irreducible`, `NonemptyInterval.coe_one_interval`, `lt_add_one_iff`, `ringKrullDim_quotSMulTop_succ_eq_ringKrullDim_of_mem_jacobson`, `ringKrullDim_succ_le_ringKrullDim_powerseries`, `unbot_one`, `one_lt_coe`, `Polynomial.degree_X_sub_C`, `ringKrullDim_quotSMulTop_succ_eq_ringKrullDim`, `Order.krullDim_le_of_krullDim_preimage_le`, `Interval.one_mem_one`, `Polynomial.Splits.degree_eq_one_of_irreducible`, `Module.supportDim_quotSMulTop_succ_eq_of_notMem_minimalPrimes_of_mem_maximalIdeal`, `ringKrullDim_succ_le_of_surjective`, `Polynomial.degree_X_le`, `Nat.WithBot.add_eq_one_iff`, `Module.ringKrullDim_quotient_add_one_of_mem_nonZeroDivisors`, `Order.krullDim_WithTop`, `Polynomial.Splits.def`, `succ_one`, `Nat.WithBot.add_eq_three_iff`, `Lagrange.degree_basisDivisor_of_ne`, `Ideal.height_le_ringKrullDim_quotient_add_one`, `Polynomial.splits_iff`, `map_one`, `Polynomial.degree_C_lt`, `Order.krullDim_le_one_iff_of_boundedOrder`, `Polynomial.degree_X_sub_C_le`, `Polynomial.degree_C_mul_X_le`, `Interval.coe_one`, `withBotSucc_one`, `ringKrullDim_quotient_span_singleton_succ_eq_ringKrullDim_of_mem_nonZeroDivisors`, `Module.supportDim_quotSMulTop_succ_eq_supportDim`, `Nat.WithBot.one_le_iff_zero_lt`, `ringKrullDim_quotient_succ_le_of_nonZeroDivisor`, `ringKrullDim_quotient_span_singleton_succ_eq_ringKrullDim_of_mem_jacobson`, `IsPrincipalIdealRing.ringKrullDim_eq_one`, `Polynomial.Splits.splits`, `Order.one_le_krullDim_iff`, `Cubic.degree_of_c_ne_zero`, `Module.supportDim_le_supportDim_quotSMulTop_succ`, `Polynomial.degree_X`, `Module.supportDim_quotSMulTop_succ_eq_supportDim_mem_jacobson`, `Polynomial.ringKrullDim_le`, `unbotD_one`, `Nat.WithBot.lt_one_iff_le_zero`, `minpoly.degree_eq_one_iff`, `IsSepClosed.degree_eq_one_of_irreducible`, `one_eq_coe`, `Order.krullDim_le_one_iff_forall_isMax`, `Order.krullDim_withBot`, `Polynomial.degree_eq_one_of_irreducible_of_splits`, `coe_one`, `Module.supportDim_le_supportDim_quotSMulTop_succ_of_mem_jacobson`, `Interval.pure_one`, `Nat.WithBot.add_one_le_of_lt`, `Polynomial.degree_eq_one_of_irreducible_of_root`, `Polynomial.degree_mul_X`, `Interval.mul_eq_one_iff`, `Cubic.degree_of_b_eq_zero'`, `Cubic.degree_of_c_ne_zero'`, `Polynomial.degree_linear_le`, `Order.krullDim_eq_one_iff_of_boundedOrder`, `Polynomial.degree_C_mul_X`, `Order.krullDim_le_one_iff_forall_isMin`, `Polynomial.ringKrullDim_of_isNoetherianRing`, `OneHom.withBotMap_apply`, `Polynomial.splits_iff_splits`, `Module.supportDim_quotSMulTop_succ_eq_of_notMem_minimalPrimes_of_mem_jacobson`, `IsAlgClosed.degree_eq_one_of_irreducible`, `Order.krullDim_of_isSimpleOrder`, `ringKrullDim_le_ringKrullDim_quotSMulTop_succ`, `Module.supportDim_quotSMulTop_succ_le_of_notMem_minimalPrimes`, `bot_lt_one`, `Polynomial.degree_linear`, `Order.krullDim_le_of_krullDim_preimage_le'`, `Finset.max_one`, `one_le_iff_pos`, `one_eq_map_iff`, `coe_le_one`, `one_le_coe`, `Polynomial.degree_X_add_C`, `add_one_le_iff`
`zero` 📖	CompOp	109 math math: `mul_bot'`, `IsAlgClosed.roots_eq_zero_iff_degree_nonpos`, `instPosMulStrictMono`, `coe_le_zero`, `zeroLEOneClass`, `instMulPosMono`, `Order.krullDim_nonneg_iff`, `Polynomial.zero_le_degree_iff`, `Order.krullDim_pos_iff`, `coe_eq_zero`, `Nat.WithBot.add_eq_two_iff`, `Polynomial.degree_list_prod`, `Order.krullDim_eq_zero_of_unique`, `minpoly.degree_pos`, `Polynomial.tendsto_atTop_iff_leadingCoeff_nonneg`, `Polynomial.degree_list_prod_le`, `Polynomial.degree_pos_of_root`, `Order.krullDim_nonpos_iff_forall_isMax`, `map_eq_zero_iff`, `ringKrullDim_nonneg_of_nontrivial`, `ringKrullDimZero_iff_ringKrullDim_eq_zero`, `Order.krullDim_nonpos_iff_forall_isMin`, `Polynomial.tendsto_atBot_iff_leadingCoeff_nonpos`, `instPosMulReflectLE`, `Polynomial.abs_tendsto_atTop_iff`, `Polynomial.degree_C`, `LaurentPolynomial.degree_C`, `coe_pos`, `instMulPosStrictMono`, `topologicalKrullDim_zero_of_discreteTopology`, `Interval.coe_zero`, `unbot_zero`, `Interval.pure_zero`, `Polynomial.abs_tendsto_atBot_iff`, `coe_lt_zero`, `zero_eq_coe`, `Cubic.degree_of_d_ne_zero`, `Interval.add_eq_zero_iff`, `Nat.WithBot.add_eq_one_iff`, `Order.krullDim_nonpos_of_subsingleton`, `Nat.WithBot.add_eq_three_iff`, `Polynomial.degree_pos_of_ne_zero_of_nonunit`, `withBotSucc_zero`, `Irreducible.degree_pos`, `instPosMulMono`, `Polynomial.Monic.degree_pos`, `bot_neg`, `Polynomial.rootOfSplits'_eq_rootOfSplits`, `Polynomial.degree_intCast_le`, `Nat.WithBot.lt_zero_iff`, `Finset.max_zero`, `mul_def`, `bot_mul'`, `Nat.WithBot.one_le_iff_zero_lt`, `Polynomial.degree_one_le`, `Polynomial.tendsto_nhds_iff`, `coe_nonneg`, `succ_zero`, `Order.krullDim_eq_zero_iff_of_orderTop`, `Polynomial.degree_one`, `Polynomial.degree_zero_le`, `Polynomial.Monic.degree_pos_of_not_isUnit`, `ringKrullDim_eq_zero_of_isField`, `instNoZeroDivisors`, `Polynomial.isBoundedUnder_abs_atBot_iff`, `Polynomial.degree_pos_of_not_isUnit_of_dvd_monic`, `Polynomial.mem_closure_X_union_C`, `Interval.length_zero`, `Polynomial.degree_eq_zero_of_isUnit`, `Nat.WithBot.lt_one_iff_le_zero`, `NonemptyInterval.coe_zero_interval`, `Polynomial.isBoundedUnder_abs_atTop_iff`, `Order.krullDim_pos_iff_of_orderTop`, `instMulPosReflectLT`, `LaurentPolynomial.degree_C_ite`, `Order.krullDim_eq_zero`, `Polynomial.degree_le_zero_iff`, `Order.krullDim_pos_iff_of_orderBot`, `Polynomial.isUnit_iff_degree_eq_zero`, `Polynomial.degree_pos_of_aeval_root`, `unbotD_zero`, `zero_eq_map_iff`, `Interval.zero_mem_zero`, `Polynomial.abs_isBoundedUnder_iff`, `instMulPosReflectLE`, `Polynomial.natDegree_eq_zero_iff_degree_le_zero`, `Nat.WithBot.add_eq_zero_iff`, `Polynomial.degree_leadingCoeff_inv`, `Polynomial.degree_pos_of_irreducible`, `Cubic.degree_of_d_ne_zero'`, `ZeroHom.withBotMap_apply`, `Order.krullDim_nonneg`, `Polynomial.degree_cyclotomic_pos`, `Polynomial.degree_pos_of_eval₂_root`, `ringKrullDim_eq_zero_of_field`, `Cubic.degree_of_c_eq_zero`, `Polynomial.natDegree_pos_iff_degree_pos`, `Cubic.degree_of_c_eq_zero'`, `instPosMulReflectLT`, `Nat.WithBot.coe_nonneg`, `map_zero`, `Order.krullDim_eq_zero_iff_of_orderBot`, `Polynomial.Monic.degree_le_zero_iff_eq_one`, `one_le_iff_pos`, `LaurentPolynomial.degree_C_le`, `Polynomial.degree_natCast_le`, `Polynomial.degree_coe_units`, `coe_zero`, `Polynomial.degree_C_le`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`addLECancellable_coe` 📖	mathematical	—	`AddLECancellable` `WithBot` `add` `instLE` `some`	—	`addLECancellable_of_ne_bot` `coe_ne_bot`
`addLECancellable_iff_ne_bot` 📖	mathematical	—	`AddLECancellable` `WithBot` `add` `Preorder.toLE` `instPreorder`	—	`LT.lt.not_ge` `bot_lt_coe` `add_bot` `addLECancellable_of_ne_bot`
`addLECancellable_of_lt_bot` 📖	mathematical	`WithBot` `Preorder.toLT` `instPreorder` `Bot.bot` `bot`	`AddLECancellable` `add` `Preorder.toLE`	—	`addLECancellable_of_ne_bot` `LT.lt.ne`
`addLECancellable_of_ne_bot` 📖	mathematical	—	`AddLECancellable` `WithBot` `add` `instLE`	—	`le_of_add_le_add_left`
`addLeftMono` 📖	mathematical	—	`AddLeftMono` `WithBot` `add` `instLE`	—	`add_bot` `add_le_add_right`
`addLeftReflectLT` 📖	mathematical	—	`AddLeftReflectLT` `WithBot` `add` `instLT`	—	`add_bot` `instIsEmptyFalse` `lt_of_add_lt_add_left`
`addRightMono` 📖	mathematical	—	`AddRightMono` `WithBot` `add` `instLE`	—	`add_bot` `add_le_add_left`
`addRightReflectLT` 📖	mathematical	—	`AddRightReflectLT` `WithBot` `add` `instLT`	—	`add_bot` `instIsEmptyFalse` `lt_of_add_lt_add_right`
`add_bot` 📖	mathematical	—	`WithBot` `add` `Bot.bot` `bot`	—	—
`add_coe_eq_bot_iff` 📖	mathematical	—	`WithBot` `add` `some` `Bot.bot` `bot`	—	—
`add_eq_bot` 📖	mathematical	—	`WithBot` `add` `Bot.bot` `bot`	—	`add_bot`
`add_eq_coe` 📖	mathematical	—	`WithBot` `add` `some`	—	`add_bot`
`add_le_add_iff_left` 📖	mathematical	—	`WithBot` `instLE` `add`	—	`le_of_add_le_add_left` `add_le_add_right` `addLeftMono`
`add_le_add_iff_right` 📖	mathematical	—	`WithBot` `instLE` `add`	—	`le_of_add_le_add_right` `add_le_add_left` `addRightMono`
`add_le_add_iff_right'` 📖	mathematical	—	`WithBot` `WithTop` `instLE` `WithTop.instLE` `add` `WithTop.add`	—	—
`add_left_cancel` 📖	—	`WithBot` `add`	—	—	—
`add_left_inj` 📖	mathematical	—	`WithBot` `add`	—	`CanLift.prf` `canLift` `add_bot`
`add_lt_add_iff_left` 📖	mathematical	—	`WithBot` `instLT` `add`	—	`lt_of_add_lt_add_left` `addLeftReflectLT` `add_lt_add_left`
`add_lt_add_iff_right` 📖	mathematical	—	`WithBot` `instLT` `add`	—	`lt_of_add_lt_add_right` `addRightReflectLT` `add_lt_add_right`
`add_lt_add_left` 📖	mathematical	`WithBot` `instLT`	`add`	—	`CanLift.prf` `canLift` `add_bot` `add_lt_add_right`
`add_lt_add_of_le_of_lt` 📖	mathematical	`WithBot` `Preorder.toLE` `instPreorder` `Preorder.toLT`	`add`	—	`LT.lt.trans_le` `add_lt_add_left` `add_le_add_left` `addRightMono`
`add_lt_add_of_lt_of_le` 📖	mathematical	`WithBot` `Preorder.toLT` `instPreorder` `Preorder.toLE`	`add`	—	`LT.lt.trans_le` `add_lt_add_right` `add_le_add_right` `addLeftMono`
`add_lt_add_right` 📖	mathematical	`WithBot` `instLT`	`add`	—	`CanLift.prf` `canLift` `add_lt_add_left`
`add_ne_bot` 📖	—	—	—	—	`add_bot`
`add_right_cancel` 📖	—	`WithBot` `add`	—	—	—
`add_right_inj` 📖	mathematical	—	`WithBot` `add`	—	`CanLift.prf` `canLift`
`bot_add` 📖	mathematical	—	`WithBot` `add` `Bot.bot` `bot`	—	—
`bot_lt_add` 📖	mathematical	—	`WithBot` `instLT` `Bot.bot` `bot` `add`	—	—
`bot_lt_natCast` 📖	mathematical	—	`WithBot` `instLT` `Bot.bot` `bot` `AddMonoidWithOne.toNatCast` `addMonoidWithOne`	—	`bot_lt_coe`
`bot_lt_one` 📖	mathematical	—	`WithBot` `instLT` `Bot.bot` `bot` `one`	—	`bot_lt_coe`
`bot_ne_natCast` 📖	—	—	—	—	`bot_ne_coe`
`bot_ne_ofNat` 📖	—	—	—	—	`bot_ne_natCast`
`bot_ne_one` 📖	—	—	—	—	`bot_ne_coe`
`bot_ne_zero` 📖	—	—	—	—	`bot_ne_coe`
`bot_neg` 📖	mathematical	—	`WithBot` `instLT` `Bot.bot` `bot` `zero`	—	`bot_lt_coe`
`charZero` 📖	mathematical	—	`CharZero` `WithBot` `addMonoidWithOne`	—	`WithTop.charZero`
`coe_add` 📖	mathematical	—	`some` `WithBot` `add`	—	—
`coe_addHom` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `WithBot` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `addZeroClass` `AddMonoidHom.instFunLike` `addHom` `some`	—	—
`coe_add_eq_bot_iff` 📖	mathematical	—	`WithBot` `add` `some` `Bot.bot` `bot`	—	—
`coe_eq_ofNat` 📖	mathematical	—	`some`	—	`coe_eq_coe`
`coe_eq_one` 📖	mathematical	—	`some` `WithBot` `one`	—	`coe_eq_coe`
`coe_eq_zero` 📖	mathematical	—	`some` `WithBot` `zero`	—	`coe_eq_coe`
`coe_le_one` 📖	mathematical	—	`WithBot` `instLE` `some` `one`	—	`coe_le_coe`
`coe_le_zero` 📖	mathematical	—	`WithBot` `instLE` `some` `zero`	—	`coe_le_coe`
`coe_lt_one` 📖	mathematical	—	`WithBot` `instLT` `some` `one`	—	`coe_lt_coe`
`coe_lt_zero` 📖	mathematical	—	`WithBot` `instLT` `some` `zero`	—	`coe_lt_coe`
`coe_natCast` 📖	mathematical	—	`some` `AddMonoidWithOne.toNatCast` `WithBot` `addMonoidWithOne`	—	—
`coe_nonneg` 📖	mathematical	—	`WithBot` `instLE` `zero` `some`	—	`coe_le_coe`
`coe_nsmul` 📖	mathematical	—	`some` `AddMonoid.toNatSMul` `WithBot` `addMonoid`	—	`AddMonoidHom.map_nsmul`
`coe_ofNat` 📖	mathematical	—	`some`	—	—
`coe_one` 📖	mathematical	—	`some` `WithBot` `one`	—	—
`coe_pos` 📖	mathematical	—	`WithBot` `instLT` `zero` `some`	—	`coe_lt_coe`
`coe_zero` 📖	mathematical	—	`some` `WithBot` `zero`	—	—
`le_of_add_le_add_left` 📖	—	`WithBot` `instLE` `add`	—	—	`CanLift.prf` `canLift` `add_bot` `le_of_add_le_add_left`
`le_of_add_le_add_right` 📖	—	`WithBot` `instLE` `add`	—	—	`CanLift.prf` `canLift` `le_of_add_le_add_right`
`map_add` 📖	mathematical	—	`map` `DFunLike.coe` `WithBot` `add`	—	`bot_add` `add_bot` `map_coe` `coe_add` `map_add`
`map_eq_natCast_iff` 📖	mathematical	—	`map` `WithBot` `AddMonoidWithOne.toNatCast` `addMonoidWithOne` `some`	—	`map_eq_some_iff`
`map_eq_ofNat_iff` 📖	mathematical	—	`map` `some` `AddMonoidWithOne.toNatCast`	—	`map_eq_some_iff`
`map_eq_one_iff` 📖	mathematical	—	`map` `WithBot` `one` `some`	—	`map_eq_some_iff`
`map_eq_zero_iff` 📖	mathematical	—	`map` `WithBot` `zero` `some`	—	`map_eq_some_iff`
`map_natCast` 📖	mathematical	—	`map` `WithBot` `AddMonoidWithOne.toNatCast` `addMonoidWithOne` `some`	—	`map_coe`
`map_ofNat` 📖	mathematical	—	`map` `some`	—	`map_coe`
`map_one` 📖	mathematical	—	`map` `WithBot` `one` `some`	—	—
`map_zero` 📖	mathematical	—	`map` `WithBot` `zero` `some`	—	—
`natCast_eq_map_iff` 📖	mathematical	—	`WithBot` `AddMonoidWithOne.toNatCast` `addMonoidWithOne` `map` `some`	—	`some_eq_map_iff`
`natCast_ne_bot` 📖	—	—	—	—	`coe_ne_bot`
`ofNat_eq_coe` 📖	mathematical	—	`some`	—	`coe_eq_coe`
`ofNat_eq_map_iff` 📖	mathematical	—	`map` `some` `AddMonoidWithOne.toNatCast`	—	`some_eq_map_iff`
`ofNat_ne_bot` 📖	—	—	—	—	`natCast_ne_bot`
`one_eq_coe` 📖	mathematical	—	`WithBot` `one` `some`	—	`coe_eq_one`
`one_eq_map_iff` 📖	mathematical	—	`WithBot` `one` `map` `some`	—	`some_eq_map_iff`
`one_le_coe` 📖	mathematical	—	`WithBot` `instLE` `one` `some`	—	`coe_le_coe`
`one_lt_coe` 📖	mathematical	—	`WithBot` `instLT` `one` `some`	—	`coe_lt_coe`
`one_ne_bot` 📖	—	—	—	—	`coe_ne_bot`
`unbotD_one` 📖	mathematical	—	`unbotD` `WithBot` `one`	—	—
`unbotD_zero` 📖	mathematical	—	`unbotD` `WithBot` `zero`	—	—
`unbot_one` 📖	mathematical	—	`unbot` `WithBot` `one` `coe_ne_bot`	—	`coe_ne_bot`
`unbot_zero` 📖	mathematical	—	`unbot` `WithBot` `zero` `coe_ne_bot`	—	`coe_ne_bot`
`zeroLEOneClass` 📖	mathematical	—	`ZeroLEOneClass` `WithBot` `zero` `one` `instLE`	—	`coe_le_coe` `zero_le_one`
`zero_eq_coe` 📖	mathematical	—	`WithBot` `zero` `some`	—	`coe_eq_zero`
`zero_eq_map_iff` 📖	mathematical	—	`WithBot` `zero` `map` `some`	—	`some_eq_map_iff`
`zero_ne_bot` 📖	—	—	—	—	`coe_ne_bot`

WithTop

Definitions

Name	Category	Theorems
`add` 📖	CompOp	79 math math: `WithBot.add_le_add_iff_right'`, `MeasureTheory.IsStoppingTime.add`, `Associates.factors_mul`, `meromorphicOrderAt_mul`, `Tropical.instNoZeroDivisorsWithTop`, `MeasureTheory.IsStoppingTime.add_const'`, `ENat.coe_top_add_one`, `addLECancellable_coe`, `AddHom.withTopMap_apply`, `instOrderedSub`, `contDiff_succ_iff_fderiv`, `AddHom.ENatMap_apply`, `add_eq_coe`, `HahnSeries.orderTop_mul_of_nonzero`, `MvPowerSeries.lexOrder_mul`, `Tropical.mul_eq_zero_iff`, `contDiffOn_succ_of_fderivWithin`, `add_lt_top`, `contDiffOn_succ_iff_fderiv_of_isOpen`, `add_lt_add_right`, `add_lt_add_of_lt_of_le`, `hasFTaylorSeriesUpToOn_succ_iff_right`, `existsAddOfLE`, `Associates.prod_add`, `addLeftReflectLT`, `untop₀_add`, `addRightReflectLT`, `add_eq_top`, `HahnSeries.orderTop_mul_of_ne_zero`, `add_top`, `contDiffWithinAt_succ_iff_hasFDerivWithinAt'`, `contDiffOn_succ_iff_hasFDerivWithinAt`, `coe_add_eq_top_iff`, `meromorphicOrderAt_smul`, `contDiffOn_succ_iff_deriv_of_isOpen`, `add_right_inj`, `tangentBundleCore.isContMDiff`, `contDiff_succ_iff_fderiv_apply`, `ENat.add_one_eq_coe_top_iff`, `TangentBundle.contMDiffVectorBundle`, `contDiffAt_succ_iff_hasFDerivAt`, `HahnSeries.orderTop_mul`, `HahnSeries.orderTop_add_le_mul`, `top_add`, `canonicallyOrderedAdd`, `add_lt_add`, `add_lt_add_iff_right`, `hasFTaylorSeriesUpToOn_succ_iff_left`, `contDiffOn_succ_iff_fderivWithin`, `add_coe_eq_top_iff`, `Padic.AddValuation.map_mul`, `contDiffOn_succ_iff_fderiv_apply`, `ENat.map_add`, `contDiff_succ_iff_deriv`, `contDiffOn_succ_iff_derivWithin`, `Associates.FactorSet.coe_add`, `addRightMono`, `contDiffOn_succ_iff_hasFDerivWithinAt_of_uniqueDiffOn`, `add_lt_add_left`, `minSmoothness_add`, `MeasureTheory.IsStoppingTime.add_const`, `contDiffOn_succ_of_fderiv_apply`, `addLeftMono`, `coe_add`, `untopD_add`, `MvPowerSeries.le_lexOrder_mul`, `addLECancellable_of_lt_top`, `Associates.FactorSet.sup_add_inf_eq_add`, `addLECancellable_of_ne_top`, `add_lt_add_iff_left`, `addLECancellable_iff_ne_top`, `add_le_add_iff_left`, `add_lt_add_of_le_of_lt`, `add_left_inj`, `contDiff_succ_iff_hasFDerivAt`, `MvPowerSeries.lexOrder_mul_ge`, `contDiffWithinAt_succ_iff_hasFDerivWithinAt`, `add_le_add_iff_right`, `map_add`
`addCommMonoid` 📖	CompOp	4 math math: `isOrderedAddMonoid`, `sum_eq_top`, `coe_sum`, `sum_lt_top`
`addCommMonoidWithOne` 📖	CompOp	—
`addCommSemigroup` 📖	CompOp	—
`addHom` 📖	CompOp	1 math math: `coe_addHom`
`addMonoid` 📖	CompOp	3 math math: `Associates.pow_factors`, `HahnSeries.orderTop_nsmul_le_orderTop_pow`, `coe_nsmul`
`addMonoidWithOne` 📖	CompOp	89 math math: `TangentBundle.continuousLinearMapAt_model_space`, `contMDiffWithinAt_vectorSpace_iff_contDiffWithinAt`, `ENat.some_eq_coe`, `charZero`, `MeasureTheory.smul_le_stoppedValue_hittingBtwn`, `untop₀_natCast`, `contMDiff_addInvariantVectorField`, `ENat.natCast_le_of_coe_top_le_withTop`, `MeasureTheory.StronglyAdapted.isStoppingTime_upperCrossingTime`, `contMDiff_mulInvariantVectorField`, `Real.contDiffAt_rpow_const_of_le`, `contMDiff_infty`, `contDiffOn_nat_iff_continuousOn_differentiableOn_deriv`, `Nat.cast_withTop`, `contDiffWithinAt_nat`, `contDiffOn_infty`, `tangentBundle_model_space_coe_chartAt`, `contDiff_iff_forall_nat_le`, `contMDiffAt_mulInvariantVectorField`, `mdifferentiableAt_addInvariantVectorField`, `contDiff_all_iff_nat`, `mdifferentiable_mulInvariantVectorField`, `contDiffOn_nat_iff_continuousOn_differentiableOn`, `MeasureTheory.stoppedValue_lowerCrossingTime`, `contMDiff_vectorSpace_iff_contDiff`, `TangentBundle.coordChange_model_space`, `map_eq_natCast_iff`, `contDiff_nat_iff_iteratedDeriv`, `contDiffPointwiseHolderAt_iff`, `trivializationAt_model_space_apply`, `hasFTaylorSeriesUpToOn_top_iff`, `hasFTaylorSeriesUpTo_succ_nat_iff_right`, `MeasureTheory.StronglyAdapted.isStoppingTime_crossing`, `MeasureTheory.stoppedValue_upperCrossingTime`, `hasFTaylorSeriesUpToOn_succ_nat_iff_right`, `instIsContMDiffRiemannianBundleOfNatWithTopENat_2`, `natCast_eq_map_iff`, `MeasureTheory.smul_le_stoppedValue_hitting`, `tangentBundle_model_space_coe_chartAt_symm`, `tangentBundleModelSpaceHomeomorph_coe`, `tangentBundleCore_coordChange_model_space`, `contDiffOn_all_iff_nat`, `instIsManifoldMinSmoothnessOfNatWithTopENat`, `PeriodPair.order_weierstrassP`, `contDiffOn_iff_forall_nat_le`, `contDiffAt_succ_iff_hasFDerivAt`, `contDiffWithinAt_infty`, `tangentBundle_model_space_chartAt`, `contMDiffAt_iff_nat`, `Real.contDiffAt_rpow_const`, `MeasureTheory.le_sub_of_le_upcrossingsBefore`, `natCast_lt_top`, `contMDiffAt_vectorSpace_iff_contDiffAt`, `mdifferentiable_addInvariantVectorField`, `contDiffAt_infty`, `VectorField.contMDiffWithinAt_mpullbackWithin_extChartAt_symm`, `TangentBundle.symmL_model_space`, `contDiff_nat_iff_continuous_differentiable`, `contDiffWithinAt_iff_forall_nat_le`, `tangentBundleModelSpaceHomeomorph_coe_symm`, `meromorphicOrderAt_pow`, `hasFTaylorSeriesUpToOn_succ_iff_left`, `Real.contDiff_rpow_const_of_le`, `ContDiffPointwiseHolderAt.contDiffAt`, `hasFTaylorSeriesUpTo_top_iff`, `mdifferentiableAt_mulInvariantVectorField`, `contMDiffWithinAt_infty`, `IsManifold.instOfNatWithTopENat_2`, `MeasureTheory.StronglyAdapted.isStoppingTime_lowerCrossingTime`, `map_natCast`, `contDiff_infty`, `contMDiffAt_addInvariantVectorField`, `contMDiff_tangentBundleModelSpaceHomeomorph`, `contMDiffAt_infty`, `contMDiff_tangentBundleModelSpaceHomeomorph_symm`, `MeasureTheory.sub_eq_zero_of_upcrossingsBefore_lt`, `coe_natCast`, `ContDiffPointwiseHolderAt.zero_exponent_iff`, `VectorField.eventually_contMDiffWithinAt_mpullbackWithin_extChartAt_symm`, `IsManifold.instLEInftyCastWithTopENat`, `contMDiffOn_vectorSpace_iff_contDiffOn`, `inTangentCoordinates_model_space`, `contMDiffWithinAt_iff_nat`, `ENat.natCast_lt_of_coe_top_le_withTop`, `hasFTaylorSeriesUpToOn_top_iff_add`, `inCoordinates_tangent_bundle_core_model_space`, `contMDiff_snd_tangentBundle_modelSpace`, `contMDiffOn_infty`, `contDiff_succ_iff_hasFDerivAt`
`addSemigroup` 📖	CompOp	—
`addZeroClass` 📖	CompOp	3 math math: `AddMonoidHom.withTopMap_apply`, `AddMonoidHom.ENatMap_apply`, `coe_addHom`
`one` 📖	CompOp	66 math math: `instContMDiffVectorBundleOfNatWithTopENatTangentSpaceOfIsManifold`, `instLieAddGroupOfNatWithTopENat`, `OneHom.withTopMap_apply`, `instIsContMDiffRiemannianBundleOfNatWithTopENat_1`, `one_eq_map_iff`, `ENat.coe_top_add_one`, `contDiff_one_iff_fderiv`, `contMDiff_equivTangentBundleProd_symm`, `one_lt_top`, `one_lt_coe`, `contDiff_succ_iff_fderiv`, `IsContDiffImplicitAt.one_le`, `contDiffAt_one_iff`, `contDiffOn_succ_of_fderivWithin`, `Finset.min_one`, `meromorphicOrderAt_id`, `instContMDiffInv₀OfNatWithTopENat`, `contDiffOn_succ_iff_fderiv_of_isOpen`, `hasFTaylorSeriesUpToOn_succ_iff_right`, `instIsManifoldMinSmoothnessOfNatWithTopENat_1`, `instContMDiffVectorBundleOfNatWithTopENat`, `zeroLEOneClass`, `coe_one`, `ENat.one_le_iff_ne_zero_withTop`, `contDiffWithinAt_succ_iff_hasFDerivWithinAt'`, `contDiffOn_succ_iff_hasFDerivWithinAt`, `coe_eq_one`, `IsManifold.instLEInftyOfNatWithTopENat_1`, `contDiffOn_succ_iff_deriv_of_isOpen`, `instContMDiffMulOfNatWithTopENat`, `Manifold.riemannianEDist_def`, `tangentBundleCore.isContMDiff`, `contDiff_succ_iff_fderiv_apply`, `ENat.add_one_eq_coe_top_iff`, `TangentBundle.contMDiffVectorBundle`, `contDiffAt_succ_iff_hasFDerivAt`, `coe_lt_one`, `map_eq_one_iff`, `coe_le_one`, `differentiableWithinAt_localInvariantProp`, `contDiff_one_iff_hasFDerivAt`, `contMDiff_equivTangentBundleProd`, `instIsManifoldOfNatWithTopENatOfMinSmoothness_1`, `hasFTaylorSeriesUpToOn_succ_iff_left`, `contDiffOn_succ_iff_fderivWithin`, `contDiffOn_succ_iff_fderiv_apply`, `one_eq_coe`, `contDiff_succ_iff_deriv`, `IsManifold.instOfNatWithTopENat_1`, `contDiffOn_succ_iff_derivWithin`, `instContMDiffAddOfNatWithTopENat`, `contDiffOn_succ_iff_hasFDerivWithinAt_of_uniqueDiffOn`, `untop_one`, `one_le_coe`, `contDiffOn_succ_of_fderiv_apply`, `untopD_one`, `contDiff_norm_rpow`, `exists_continuousLinearEquiv_fderiv_symm_eq`, `Manifold.exists_lt_of_riemannianEDist_lt`, `exists_continuousLinearEquiv_fderivWithin_symm_eq`, `Manifold.exists_lt_locally_constant_of_riemannianEDist_lt`, `instLieGroupOfNatWithTopENat`, `map_one`, `contDiff_succ_iff_hasFDerivAt`, `contDiff_one_iff_deriv`, `contDiffWithinAt_succ_iff_hasFDerivWithinAt`
`zero` 📖	CompOp	95 math math: `ValueDistribution.logCounting_zero`, `instContMDiffAddOfNatWithTopENatOfContinuousAdd`, `tendsto_zero_iff_meromorphicOrderAt_pos`, `MeromorphicOn.codiscrete_setOf_meromorphicOrderAt_eq_zero_or_top`, `ValueDistribution.proximity_zero`, `meromorphicOrderAt_const_ofNat`, `Finset.min_zero`, `tendsto_cobounded_iff_meromorphicOrderAt_neg`, `meromorphicOrderAt_const`, `Padic.AddValuation.map_one`, `mul_def`, `top_mul'`, `ValueDistribution.logCounting_zero_mul_le`, `ValueDistribution.proximity_zero_mul_le`, `HahnSeries.orderTop_sub_pos`, `MeromorphicNFAt.meromorphicOrderAt_nonneg_iff_analyticAt`, `instLieGroupOfNatWithTopENatOfIsTopologicalGroup`, `untop₀_zero`, `instContMDiffInv₀OfNatWithTopENatOfContinuousInv₀`, `contDiff_zero`, `ValueDistribution.proximity_pow_zero`, `IsManifold.instLEInftyOfNatWithTopENat_2`, `ZeroHom.withTopMap_apply`, `ValueDistribution.logCounting_coe_eq_logCounting_sub_const_zero`, `ValueDistribution.proximity_coe_eq_proximity_sub_const_zero`, `ValueDistribution.logCounting_mul_zero_eventuallyLE`, `HahnSeries.orderTop_one`, `ENat.map_natCast_eq_zero`, `ValueDistribution.proximity_inv`, `instLieAddGroupOfNatWithTopENatOfIsTopologicalAddGroup`, `hasFTaylorSeriesUpTo_zero_iff`, `coe_le_zero`, `untop₀_nonneg`, `untop_zero`, `coe_eq_zero`, `HahnSeries.zero_lt_orderTop_of_order`, `Associates.count_zero`, `contDiffWithinAt_zero`, `contMDiff_zero_iff`, `meromorphicOrderAt_const_natCast`, `AnalyticAt.meromorphicOrderAt_nonneg`, `hasFTaylorSeriesUpToOn_zero_iff`, `tendsto_nhds_iff_meromorphicOrderAt_nonneg`, `ValueDistribution.proximity_mul_zero_le`, `map_zero`, `meromorphicNFAt_iff_analyticAt_or`, `coe_zero`, `zeroLEOneClass`, `Real.contDiffAt_arcsin_iff`, `contDiffOn_zero`, `untopD_zero`, `HahnSeries.unit_aux`, `ValueDistribution.characteristic_mul_zero_eventuallyLE`, `ValueDistribution.characteristic_pow_zero`, `tendsto_ne_zero_iff_meromorphicOrderAt_eq_zero`, `contDiffGroupoid_zero_eq`, `mul_top'`, `ValueDistribution.characteristic_mul_zero_le`, `locallyFinsuppWithin.logCounting_divisor`, `ValueDistribution.logCounting_zero_mul_eventually_le`, `ValueDistribution.proximity_zero_of_complexValued`, `ValueDistribution.characteristic_zero_mul_eventually_le`, `map_eq_zero_iff`, `zero_eq_map_iff`, `instContMDiffVectorBundleOfNatWithTopENat_1`, `ENat.map_natCast_nonneg`, `ValueDistribution.characteristic_zero_mul_le`, `HahnSeries.SummableFamily.powers_toFun`, `instIsContMDiffRiemannianBundleOfNatWithTopENat`, `coe_nonneg`, `HahnSeries.orderTop_self_sub_one_pos_iff`, `ValueDistribution.logCounting_pow_zero`, `contDiffAt_zero`, `instContMDiffMulOfNatWithTopENatOfContinuousMul`, `ValueDistribution.logCounting_zero_sub_logCounting_top_eq_circleAverage_sub_const`, `top_pos`, `coe_pos`, `HahnSeries.zero_lt_orderTop_iff`, `meromorphicOrderAt_of_not_meromorphicAt`, `meromorphicOrderAt_const_intCast`, `MeromorphicNFAt.meromorphicOrderAt_eq_zero_iff`, `untop₀_eq_zero`, `HahnSeries.zero_le_orderTop_iff`, `instNoZeroDivisors`, `zero_eq_coe`, `ValueDistribution.log_counting_zero_sub_logCounting_top`, `contMDiffOn_zero_iff`, `HahnSeries.mem_orderTopSubOnePos_iff`, `Associates.factors_one`, `ContDiffPointwiseHolderAt.zero_order_iff`, `ValueDistribution.logCounting_inv`, `Real.contDiffAt_arccos_iff`, `IsManifold.instOfNatWithTopENat`, `coe_lt_zero`, `ValueDistribution.logCounting_mul_zero_le`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`addLECancellable_coe` 📖	mathematical	—	`AddLECancellable` `WithTop` `add` `instLE` `some`	—	`addLECancellable_of_ne_top` `coe_ne_top`
`addLECancellable_iff_ne_top` 📖	mathematical	—	`AddLECancellable` `WithTop` `add` `Preorder.toLE` `instPreorder`	—	`LT.lt.not_ge` `coe_lt_top` `add_top` `addLECancellable_of_ne_top`
`addLECancellable_of_lt_top` 📖	mathematical	`WithTop` `Preorder.toLT` `instPreorder` `Top.top` `top`	`AddLECancellable` `add` `Preorder.toLE`	—	`addLECancellable_of_ne_top` `LT.lt.ne`
`addLECancellable_of_ne_top` 📖	mathematical	—	`AddLECancellable` `WithTop` `add` `instLE`	—	`le_of_add_le_add_left`
`addLeftMono` 📖	mathematical	—	`AddLeftMono` `WithTop` `add` `instLE`	—	`add_top` `add_le_add_right`
`addLeftReflectLT` 📖	mathematical	—	`AddLeftReflectLT` `WithTop` `add` `instLT`	—	`add_top` `instIsEmptyFalse` `lt_of_add_lt_add_left`
`addRightMono` 📖	mathematical	—	`AddRightMono` `WithTop` `add` `instLE`	—	`add_top` `add_le_add_left`
`addRightReflectLT` 📖	mathematical	—	`AddRightReflectLT` `WithTop` `add` `instLT`	—	`add_top` `instIsEmptyFalse` `lt_of_add_lt_add_right`
`add_coe_eq_top_iff` 📖	mathematical	—	`WithTop` `add` `some` `Top.top` `top`	—	—
`add_eq_coe` 📖	mathematical	—	`WithTop` `add` `some`	—	`add_top`
`add_eq_top` 📖	mathematical	—	`WithTop` `add` `Top.top` `top`	—	`add_top`
`add_le_add_iff_left` 📖	mathematical	—	`WithTop` `instLE` `add`	—	`le_of_add_le_add_left` `add_le_add_right` `addLeftMono`
`add_le_add_iff_right` 📖	mathematical	—	`WithTop` `instLE` `add`	—	`le_of_add_le_add_right` `add_le_add_left` `addRightMono`
`add_left_cancel` 📖	—	`WithTop` `add`	—	—	—
`add_left_inj` 📖	mathematical	—	`WithTop` `add`	—	`CanLift.prf` `canLift` `add_top`
`add_lt_add` 📖	mathematical	`WithTop` `Preorder.toLT` `instPreorder`	`add`	—	`LT.lt.trans_le` `add_lt_add_left` `LT.lt.ne_top` `add_top` `LT.lt.le` `add_lt_add_right` `coe_ne_top`
`add_lt_add_iff_left` 📖	mathematical	—	`WithTop` `instLT` `add`	—	`lt_of_add_lt_add_left` `addLeftReflectLT` `add_lt_add_left`
`add_lt_add_iff_right` 📖	mathematical	—	`WithTop` `instLT` `add`	—	`lt_of_add_lt_add_right` `addRightReflectLT` `add_lt_add_right`
`add_lt_add_left` 📖	mathematical	`WithTop` `instLT`	`add`	—	`CanLift.prf` `canLift` `add_top` `add_lt_add_right`
`add_lt_add_of_le_of_lt` 📖	mathematical	`WithTop` `Preorder.toLE` `instPreorder` `Preorder.toLT`	`add`	—	`LT.lt.trans_le` `add_lt_add_left` `add_le_add_left` `addRightMono`
`add_lt_add_of_lt_of_le` 📖	mathematical	`WithTop` `Preorder.toLT` `instPreorder` `Preorder.toLE`	`add`	—	`LT.lt.trans_le` `add_lt_add_right` `add_le_add_right` `addLeftMono`
`add_lt_add_right` 📖	mathematical	`WithTop` `instLT`	`add`	—	`CanLift.prf` `canLift` `add_lt_add_left`
`add_lt_top` 📖	mathematical	—	`WithTop` `instLT` `add` `Top.top` `top`	—	—
`add_ne_top` 📖	—	—	—	—	`add_top`
`add_right_cancel` 📖	—	`WithTop` `add`	—	—	—
`add_right_inj` 📖	mathematical	—	`WithTop` `add`	—	`CanLift.prf` `canLift`
`add_top` 📖	mathematical	—	`WithTop` `add` `Top.top` `top`	—	—
`charZero` 📖	mathematical	—	`CharZero` `WithTop` `addMonoidWithOne`	—	`coe_eq_coe` `Nat.cast_injective`
`coe_add` 📖	mathematical	—	`some` `WithTop` `add`	—	—
`coe_addHom` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `WithTop` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `addZeroClass` `AddMonoidHom.instFunLike` `addHom` `some`	—	—
`coe_add_eq_top_iff` 📖	mathematical	—	`WithTop` `add` `some` `Top.top` `top`	—	—
`coe_eq_ofNat` 📖	mathematical	—	`some`	—	`coe_eq_coe`
`coe_eq_one` 📖	mathematical	—	`some` `WithTop` `one`	—	`coe_eq_coe`
`coe_eq_zero` 📖	mathematical	—	`some` `WithTop` `zero`	—	`coe_eq_coe`
`coe_le_one` 📖	mathematical	—	`WithTop` `instLE` `some` `one`	—	`coe_le_coe`
`coe_le_zero` 📖	mathematical	—	`WithTop` `instLE` `some` `zero`	—	`coe_le_coe`
`coe_lt_one` 📖	mathematical	—	`WithTop` `instLT` `some` `one`	—	`coe_lt_coe`
`coe_lt_zero` 📖	mathematical	—	`WithTop` `instLT` `some` `zero`	—	`coe_lt_coe`
`coe_natCast` 📖	mathematical	—	`some` `AddMonoidWithOne.toNatCast` `WithTop` `addMonoidWithOne`	—	—
`coe_ne_one` 📖	—	—	—	—	`Iff.ne` `coe_eq_one`
`coe_ne_zero` 📖	—	—	—	—	`Iff.ne` `coe_eq_zero`
`coe_nonneg` 📖	mathematical	—	`WithTop` `instLE` `zero` `some`	—	`coe_le_coe`
`coe_nsmul` 📖	mathematical	—	`some` `AddMonoid.toNatSMul` `WithTop` `addMonoid`	—	—
`coe_ofNat` 📖	mathematical	—	`some`	—	—
`coe_one` 📖	mathematical	—	`some` `WithTop` `one`	—	—
`coe_pos` 📖	mathematical	—	`WithTop` `instLT` `zero` `some`	—	`coe_lt_coe`
`coe_zero` 📖	mathematical	—	`some` `WithTop` `zero`	—	—
`existsAddOfLE` 📖	mathematical	—	`ExistsAddOfLE` `WithTop` `add` `instLE`	—	`ExistsAddOfLE.exists_add_of_le` `coe_le_coe` `not_top_le_coe`
`le_of_add_le_add_left` 📖	—	`WithTop` `instLE` `add`	—	—	`CanLift.prf` `canLift` `add_top` `le_of_add_le_add_left`
`le_of_add_le_add_right` 📖	—	`WithTop` `instLE` `add`	—	—	`CanLift.prf` `canLift` `le_of_add_le_add_right`
`map_add` 📖	mathematical	—	`map` `DFunLike.coe` `WithTop` `add`	—	`top_add` `add_top` `map_coe` `coe_add` `map_add`
`map_eq_natCast_iff` 📖	mathematical	—	`map` `WithTop` `AddMonoidWithOne.toNatCast` `addMonoidWithOne` `some`	—	`map_eq_some_iff`
`map_eq_ofNat_iff` 📖	mathematical	—	`map` `some` `AddMonoidWithOne.toNatCast`	—	`map_eq_some_iff`
`map_eq_one_iff` 📖	mathematical	—	`map` `WithTop` `one` `some`	—	`map_eq_some_iff`
`map_eq_zero_iff` 📖	mathematical	—	`map` `WithTop` `zero` `some`	—	`map_eq_some_iff`
`map_natCast` 📖	mathematical	—	`map` `WithTop` `AddMonoidWithOne.toNatCast` `addMonoidWithOne` `some`	—	`map_coe`
`map_ofNat` 📖	mathematical	—	`map` `some`	—	`map_coe`
`map_one` 📖	mathematical	—	`map` `WithTop` `one` `some`	—	—
`map_zero` 📖	mathematical	—	`map` `WithTop` `zero` `some`	—	—
`natCast_eq_map_iff` 📖	mathematical	—	`WithTop` `AddMonoidWithOne.toNatCast` `addMonoidWithOne` `map` `some`	—	`some_eq_map_iff`
`natCast_lt_top` 📖	mathematical	—	`WithTop` `instLT` `AddMonoidWithOne.toNatCast` `addMonoidWithOne` `Top.top` `top`	—	`coe_lt_top`
`natCast_ne_top` 📖	—	—	—	—	`coe_ne_top`
`ofNat_eq_coe` 📖	mathematical	—	`some`	—	`coe_eq_coe`
`ofNat_eq_map_iff` 📖	mathematical	—	`map` `some` `AddMonoidWithOne.toNatCast`	—	`some_eq_map_iff`
`ofNat_ne_top` 📖	—	—	—	—	`natCast_ne_top`
`one_eq_coe` 📖	mathematical	—	`WithTop` `one` `some`	—	`coe_eq_one`
`one_eq_map_iff` 📖	mathematical	—	`WithTop` `one` `map` `some`	—	`some_eq_map_iff`
`one_le_coe` 📖	mathematical	—	`WithTop` `instLE` `one` `some`	—	`coe_le_coe`
`one_lt_coe` 📖	mathematical	—	`WithTop` `instLT` `one` `some`	—	`coe_lt_coe`
`one_lt_top` 📖	mathematical	—	`WithTop` `instLT` `one` `Top.top` `top`	—	`coe_lt_top`
`one_ne_top` 📖	—	—	—	—	`coe_ne_top`
`top_add` 📖	mathematical	—	`WithTop` `add` `Top.top` `top`	—	—
`top_ne_natCast` 📖	—	—	—	—	`top_ne_coe`
`top_ne_ofNat` 📖	—	—	—	—	`top_ne_natCast`
`top_ne_one` 📖	—	—	—	—	`top_ne_coe`
`top_ne_zero` 📖	—	—	—	—	`top_ne_coe`
`top_pos` 📖	mathematical	—	`WithTop` `instLT` `zero` `Top.top` `top`	—	`coe_lt_top`
`untopD_one` 📖	mathematical	—	`untopD` `WithTop` `one`	—	—
`untopD_zero` 📖	mathematical	—	`untopD` `WithTop` `zero`	—	—
`untop_one` 📖	mathematical	—	`untop` `WithTop` `one` `coe_ne_top`	—	`coe_ne_top`
`untop_zero` 📖	mathematical	—	`untop` `WithTop` `zero` `coe_ne_top`	—	`coe_ne_top`
`zeroLEOneClass` 📖	mathematical	—	`ZeroLEOneClass` `WithTop` `zero` `one` `instLE`	—	`coe_le_coe` `zero_le_one`
`zero_eq_coe` 📖	mathematical	—	`WithTop` `zero` `some`	—	`coe_eq_zero`
`zero_eq_map_iff` 📖	mathematical	—	`WithTop` `zero` `map` `some`	—	`some_eq_map_iff`
`zero_ne_top` 📖	—	—	—	—	`coe_ne_top`

ZeroHom

Definitions

Name	Category	Theorems
`withBotMap` 📖	CompOp	1 math math: `withBotMap_apply`
`withTopMap` 📖	CompOp	1 math math: `withTopMap_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`withBotMap_apply` 📖	mathematical	—	`DFunLike.coe` `ZeroHom` `WithBot` `WithBot.zero` `funLike` `withBotMap` `WithBot.map`	—	—
`withTopMap_apply` 📖	mathematical	—	`DFunLike.coe` `ZeroHom` `WithTop` `WithTop.zero` `funLike` `withTopMap` `WithTop.map`	—	—

---

← Back to Index