Ultra

📁 Source: Mathlib/Analysis/Normed/Ring/Ultra.lean

Statistics

Metric	Count
Definitions	0
Theorems nnnorm_add_one_le_max_nnnorm_one, nnnorm_intCast_le_one, nnnorm_natCast_le_one, norm_add_one_le_max_norm_one, norm_intCast_le_one, norm_natCast_le_one	6
Total	6

IsUltrametricDist

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
nnnorm_add_one_le_max_nnnorm_one 📖	mathematical	—	NNReal Preorder.toLE PartialOrder.toPreorder instPartialOrderNNReal NNNorm.nnnorm SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup SeminormedRing.toNonUnitalSeminormedRing Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing SeminormedRing.toRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne NNReal.instMax instOneNNReal	—	norm_add_one_le_max_norm_one
nnnorm_intCast_le_one 📖	mathematical	—	NNReal Preorder.toLE PartialOrder.toPreorder instPartialOrderNNReal NNNorm.nnnorm SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup SeminormedRing.toNonUnitalSeminormedRing AddGroupWithOne.toIntCast Ring.toAddGroupWithOne SeminormedRing.toRing instOneNNReal	—	Int.cast_natCast nnnorm_natCast_le_one Int.cast_negSucc nnnorm_neg
nnnorm_natCast_le_one 📖	mathematical	—	NNReal Preorder.toLE PartialOrder.toPreorder instPartialOrderNNReal NNNorm.nnnorm SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup SeminormedRing.toNonUnitalSeminormedRing AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne SeminormedRing.toRing instOneNNReal	—	Nat.cast_zero nnnorm_zero NNReal.instCanonicallyOrderedAdd Nat.cast_add Nat.cast_one max_eq_right nnnorm_add_one_le_max_nnnorm_one
norm_add_one_le_max_norm_one 📖	mathematical	—	Real Real.instLE Norm.norm SeminormedRing.toNorm Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing SeminormedRing.toRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Real.instMax Real.instOne	—	NormOneClass.norm_one norm_add_le_max
norm_intCast_le_one 📖	mathematical	—	Real Real.instLE Norm.norm SeminormedRing.toNorm AddGroupWithOne.toIntCast Ring.toAddGroupWithOne SeminormedRing.toRing Real.instOne	—	nnnorm_intCast_le_one
norm_natCast_le_one 📖	mathematical	—	Real Real.instLE Norm.norm SeminormedRing.toNorm AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne SeminormedRing.toRing Real.instOne	—	nnnorm_natCast_le_one

---

← Back to Index