Int

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

Statistics

Metric	Count
Definitions	0
Theorems enorm_natCast, nnnorm_coe_units, nnnorm_natCast, norm_coe_units, toNat_add_toNat_neg_eq_nnnorm, toNat_add_toNat_neg_eq_norm	6
Total	6

Int

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
enorm_natCast 📖	mathematical	—	ENorm.enorm ContinuousENorm.toENorm UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing instNormedCommRing SeminormedAddGroup.toContinuousENorm ENNReal AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal	—	Real.enorm_natCast
nnnorm_coe_units 📖	mathematical	—	NNNorm.nnnorm SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing instNormedCommRing Units.val instMonoid NNReal instOneNNReal	—	units_eq_one_or nnnorm_one instNormOneClass nnnorm_neg
nnnorm_natCast 📖	mathematical	—	NNNorm.nnnorm SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing instNormedCommRing NNReal AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring instSemiringNNReal	—	Real.nnnorm_natCast
norm_coe_units 📖	mathematical	—	Norm.norm NormedRing.toNorm NormedCommRing.toNormedRing instNormedCommRing Units.val instMonoid Real Real.instOne	—	coe_nnnorm nnnorm_coe_units NNReal.coe_one
toNat_add_toNat_neg_eq_nnnorm 📖	mathematical	—	NNReal Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiringNNReal AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne NNNorm.nnnorm SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing instNormedCommRing	—	Nat.cast_add NNReal.natCast_natAbs
toNat_add_toNat_neg_eq_norm 📖	mathematical	—	Real Real.instAdd Real.instNatCast Norm.norm NormedRing.toNorm NormedCommRing.toNormedRing instNormedCommRing	—	NNReal.coe_natCast toNat_add_toNat_neg_eq_nnnorm

---

← Back to Index