SeminormFromBounded

📁 Source: Mathlib/Analysis/Normed/Unbundled/SeminormFromBounded.lean

Statistics

Metric	Count
Definitions normFromBounded, seminormFromBounded, seminormFromBounded'	3
Theorems map_mul_zero_of_map_zero, map_one_ne_zero, map_pow_ne_zero, seminormFromBounded_add, seminormFromBounded_aux, seminormFromBounded_bddAbove_range, seminormFromBounded_eq_zero_iff, seminormFromBounded_ge, seminormFromBounded_isNonarchimedean, seminormFromBounded_is_norm_iff, seminormFromBounded_ker, seminormFromBounded_le, seminormFromBounded_mul, seminormFromBounded_neg, seminormFromBounded_nonneg, seminormFromBounded_nonzero, seminormFromBounded_of_mul_apply, seminormFromBounded_of_mul_is_mul, seminormFromBounded_of_mul_le, seminormFromBounded_one, seminormFromBounded_one_le, seminormFromBounded_zero	22
Total	25

(root)

Definitions

Name	Category	Theorems
normFromBounded 📖	CompOp	—
seminormFromBounded 📖	CompOp	—
seminormFromBounded' 📖	CompOp	15 math math: seminormFromBounded_ker, seminormFromBounded_of_mul_is_mul, seminormFromBounded_zero, seminormFromBounded_one_le, seminormFromBounded_of_mul_apply, seminormFromBounded_of_mul_le, seminormFromBounded_le, seminormFromBounded_neg, seminormFromBounded_eq_zero_iff, seminormFromBounded_one, seminormFromBounded_isNonarchimedean, seminormFromBounded_mul, seminormFromBounded_nonneg, seminormFromBounded_add, seminormFromBounded_ge

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
map_mul_zero_of_map_zero 📖	mathematical	Pi.hasLe Real Real.instLE Pi.instZero Real.instZero Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Real.instMul	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Real Real.instZero	—	MulZeroClass.mul_zero MulZeroClass.zero_mul le_antisymm
map_one_ne_zero 📖	—	Pi.hasLe Real Real.instLE Pi.instZero Real.instZero Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Real.instMul	—	—	Function.ne_iff LE.le.antisymm MulZeroClass.zero_mul MulZeroClass.mul_zero one_mul
map_pow_ne_zero 📖	—	Pi.hasLe Real Real.instLE Pi.instZero Real.instZero IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Real.instMul	—	—	map_one_ne_zero Function.ne_iff IsUnit.mul_val_inv one_pow MulZeroClass.mul_zero MulZeroClass.zero_mul LE.le.antisymm
seminormFromBounded_add 📖	mathematical	Pi.hasLe Real Real.instLE Pi.instZero Real.instZero Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Real.instMul Distrib.toAdd Real.instAdd	Real Real.instLE seminormFromBounded' Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Real.instAdd	—	ciSup_le AddTorsor.nonempty div_zero zero_add add_div div_le_div_iff_of_pos_right MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono Real.instIsStrictOrderedRing lt_of_le_of_ne' add_mul Distrib.rightDistribClass le_trans add_le_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid covariant_swap_add_of_covariant_add le_ciSup_of_le seminormFromBounded_bddAbove_range le_refl
seminormFromBounded_aux 📖	mathematical	Pi.hasLe Real Real.instLE Pi.instZero Real.instZero Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Real.instMul	Real Real.instLE Real.instZero Real.instMul	—	LE.le.eq_or_lt' MulZeroClass.mul_zero instReflLe le_of_not_gt Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Linarith.add_lt_of_neg_of_le Real.instIsStrictOrderedRing neg_neg_of_pos Real.instIsOrderedAddMonoid Mathlib.Tactic.Linarith.zero_lt_one Mathlib.Tactic.Linarith.sub_nonpos_of_le Real.instIsOrderedRing le_mul_iff_one_le_left IsOrderedRing.toMulPosMono MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.zero_mul mul_one Mathlib.Tactic.Ring.div_congr Mathlib.Tactic.Ring.div_pf Mathlib.Tactic.Ring.inv_single Mathlib.Tactic.Ring.inv_mul Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNNRat_inv_pos RCLike.charZero_rclike Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Tactic.Linarith.add_neg Mathlib.Tactic.Linarith.add_lt_of_le_of_neg Mathlib.Tactic.Linarith.without_one_mul Mathlib.Tactic.CancelDenoms.sub_subst div_le_iff₀ MulPosReflectLE.toMulPosReflectLT Mathlib.Tactic.Linarith.sub_neg_of_lt one_div_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono mul_nonneg IsOrderedRing.toPosMulMono le_of_lt
seminormFromBounded_bddAbove_range 📖	mathematical	Pi.hasLe Real Real.instLE Pi.instZero Real.instZero Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Real.instMul	BddAbove Real Real.instLE Set.range DivInvMonoid.toDiv Real.instDivInvMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	LE.le.eq_or_lt' div_zero seminormFromBounded_aux div_le_iff₀ MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono Real.instIsStrictOrderedRing
seminormFromBounded_eq_zero_iff 📖	mathematical	Pi.hasLe Real Real.instLE Pi.instZero Real.instZero Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Real.instMul	seminormFromBounded' Real Real.instZero	—	seminormFromBounded_ge LE.le.antisymm MulZeroClass.mul_zero seminormFromBounded_le seminormFromBounded_nonneg
seminormFromBounded_ge 📖	mathematical	Pi.hasLe Real Real.instLE Pi.instZero Real.instZero Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Real.instMul	Real Real.instLE Real.instMul AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing seminormFromBounded'	—	LE.le.antisymm MulZeroClass.mul_zero mul_one MulZeroClass.zero_mul le_refl mul_comm div_le_iff₀ MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono Real.instIsStrictOrderedRing lt_of_le_of_ne' le_ciSup seminormFromBounded_bddAbove_range
seminormFromBounded_isNonarchimedean 📖	mathematical	Pi.hasLe Real Real.instLE Pi.instZero Real.instZero Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Real.instMul IsNonarchimedean Real.linearOrder Distrib.toAdd	IsNonarchimedean Real Real.linearOrder Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing seminormFromBounded'	—	ciSup_le AddTorsor.nonempty le_max_iff div_zero div_le_div_iff_of_pos_right MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono Real.instIsStrictOrderedRing lt_of_le_of_ne' add_mul Distrib.rightDistribClass le_ciSup_of_le seminormFromBounded_bddAbove_range
seminormFromBounded_is_norm_iff 📖	mathematical	MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Real Real.instZero Pi.hasLe Real.instLE Pi.instZero Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Real.instMul Distrib.toAdd Real.instAdd NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup CommRing.toRing	MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Set.preimage Real Set Set.instSingletonSet Real.instZero	—	seminormFromBounded_ker Set.ext seminormFromBounded_zero Set.mem_singleton_iff Set.mem_preimage seminormFromBounded_eq_zero_iff
seminormFromBounded_ker 📖	mathematical	Pi.hasLe Real Real.instLE Pi.instZero Real.instZero Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Real.instMul	Set.preimage Real seminormFromBounded' Set Set.instSingletonSet Real.instZero	—	Set.ext seminormFromBounded_eq_zero_iff
seminormFromBounded_le 📖	mathematical	Pi.hasLe Real Real.instLE Pi.instZero Real.instZero Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Real.instMul	Real Real.instLE seminormFromBounded' Real.instMul	—	ciSup_le AddTorsor.nonempty LE.le.eq_or_lt' div_zero seminormFromBounded_aux div_le_iff₀ MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono Real.instIsStrictOrderedRing
seminormFromBounded_mul 📖	mathematical	Pi.hasLe Real Real.instLE Pi.instZero Real.instZero Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Real.instMul	Real Real.instLE seminormFromBounded' Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Real.instMul	—	ciSup_le AddTorsor.nonempty mul_comm mul_assoc map_mul_zero_of_map_zero seminormFromBounded_eq_zero_iff zero_div mul_nonneg IsOrderedRing.toPosMulMono Real.instIsOrderedRing seminormFromBounded_nonneg div_le_iff₀ MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono Real.instIsStrictOrderedRing lt_of_le_of_ne' le_ciSup_of_le seminormFromBounded_bddAbove_range div_mul_eq_mul_div div_nonneg PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono div_le_div_iff_of_pos_right le_refl
seminormFromBounded_neg 📖	mathematical	NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup CommRing.toRing	seminormFromBounded' NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup CommRing.toRing	—	neg_mul
seminormFromBounded_nonneg 📖	mathematical	Pi.hasLe Real Real.instLE Pi.instZero Real.instZero Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Real.instMul	Pi.hasLe Real Real.instLE Pi.instZero Real.instZero seminormFromBounded'	—	le_csSup_of_le seminormFromBounded_bddAbove_range div_nonneg PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing
seminormFromBounded_nonzero 📖	—	Pi.hasLe Real Real.instLE Pi.instZero Real.instZero Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Real.instMul	—	—	Function.ne_iff Pi.zero_apply seminormFromBounded_eq_zero_iff
seminormFromBounded_of_mul_apply 📖	mathematical	Pi.hasLe Real Real.instLE Pi.instZero Real.instZero Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Real.instMul	seminormFromBounded'	—	le_antisymm ciSup_le AddTorsor.nonempty div_zero MulZeroClass.mul_zero div_self mul_one le_refl map_one_ne_zero le_ciSup zero_div MulZeroClass.zero_mul ciSup_const
seminormFromBounded_of_mul_is_mul 📖	mathematical	Pi.hasLe Real Real.instLE Pi.instZero Real.instZero Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Real.instMul	seminormFromBounded' Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Real Real.instMul	—	seminormFromBounded_of_mul_apply mul_assoc mul_div_assoc Real.mul_iSup_of_nonneg
seminormFromBounded_of_mul_le 📖	mathematical	Pi.hasLe Real Real.instLE Pi.instZero Real.instZero Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Real.instMul AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Real.instOne	seminormFromBounded'	—	le_antisymm ciSup_le AddTorsor.nonempty div_zero div_le_iff₀ MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono Real.instIsStrictOrderedRing lt_of_le_of_ne' mul_one div_self mul_div_assoc zero_div LE.le.antisymm le_mul_iff_one_le_right IsOrderedRing.toPosMulMono Real.instIsOrderedRing PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono lt_of_le_of_ne div_one le_ciSup
seminormFromBounded_one 📖	mathematical	Pi.hasLe Real Real.instLE Pi.instZero Real.instZero Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Real.instMul	seminormFromBounded' AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Real Real.instOne	—	one_mul le_antisymm ciSup_le AddTorsor.nonempty div_zero zero_le_one Real.instZeroLEOneClass div_self le_refl map_one_ne_zero le_ciSup
seminormFromBounded_one_le 📖	mathematical	Pi.hasLe Real Real.instLE Pi.instZero Real.instZero Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Real.instMul	Real Real.instLE seminormFromBounded' AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Real.instOne	—	le_of_eq seminormFromBounded_one one_mul ciSup_le AddTorsor.nonempty div_zero Real.instZeroLEOneClass
seminormFromBounded_zero 📖	mathematical	MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Real Real.instZero	seminormFromBounded' MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Real Real.instZero	—	MulZeroClass.zero_mul zero_div ciSup_const AddTorsor.nonempty

---

← Back to Index