Int

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

Statistics

Metric	Count
Definitions instNormedAddCommGroup	1
Theorems abs_le_floor_nnreal_iff, norm_cast_real, norm_eq_abs, norm_natCast, natCast_natAbs, nnnorm_zpow_le_mul_norm, nnnorm_zsmul_le, norm_zpow_le_mul_norm, norm_zsmul_le	9
Total	10

Int

Definitions

Name	Category	Theorems
instNormedAddCommGroup 📖	CompOp	11 math math: NNReal.natCast_natAbs, nnnorm_zpow_le_mul_norm, norm_natCast, norm_eq_abs, norm_zsmul_le, norm_cast_rat, abs_le_floor_nnreal_iff, norm_zpow_le_mul_norm, hasSolidNorm, nnnorm_zsmul_le, norm_cast_real

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
abs_le_floor_nnreal_iff 📖	mathematical	—	abs instLatticeInt instAddGroup Nat.floor NNReal instSemiringNNReal instPartialOrderNNReal NNReal.instFloorSemiring Preorder.toLE PartialOrder.toPreorder NNNorm.nnnorm SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup NormedAddCommGroup.toSeminormedAddCommGroup instNormedAddCommGroup	—	abs_eq_natAbs Nat.le_floor_iff zero_le NNReal.instCanonicallyOrderedAdd NNReal.natCast_natAbs
norm_cast_real 📖	mathematical	—	Norm.norm Real Real.norm Real.instIntCast NormedAddCommGroup.toNorm instNormedAddCommGroup	—	—
norm_eq_abs 📖	mathematical	—	Norm.norm NormedAddCommGroup.toNorm instNormedAddCommGroup abs Real Real.lattice Real.instAddGroup Real.instIntCast	—	—
norm_natCast 📖	mathematical	—	Norm.norm NormedAddCommGroup.toNorm instNormedAddCommGroup Real Real.instNatCast	—	cast_natCast Nat.abs_cast Real.instIsOrderedRing

NNReal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
natCast_natAbs 📖	mathematical	—	NNReal AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring instSemiringNNReal NNNorm.nnnorm SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup NormedAddCommGroup.toSeminormedAddCommGroup Int.instNormedAddCommGroup	—	eq coe_natCast Int.cast_natCast Int.natCast_natAbs Int.cast_abs Real.instIsStrictOrderedRing Int.norm_eq_abs

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
nnnorm_zpow_le_mul_norm 📖	mathematical	—	NNReal Preorder.toLE PartialOrder.toPreorder instPartialOrderNNReal NNNorm.nnnorm SeminormedGroup.toNNNorm SeminormedCommGroup.toSeminormedGroup DivInvMonoid.toZPow Group.toDivInvMonoid SeminormedGroup.toGroup Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiringNNReal SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup NormedAddCommGroup.toSeminormedAddCommGroup Int.instNormedAddCommGroup	—	norm_zpow_le_mul_norm
nnnorm_zsmul_le 📖	mathematical	—	NNReal Preorder.toLE PartialOrder.toPreorder instPartialOrderNNReal NNNorm.nnnorm SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup SubNegMonoid.toZSMul AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiringNNReal NormedAddCommGroup.toSeminormedAddCommGroup Int.instNormedAddCommGroup	—	NNReal.coe_le_coe norm_zsmul_le
norm_zpow_le_mul_norm 📖	mathematical	—	Real Real.instLE Norm.norm SeminormedCommGroup.toNorm DivInvMonoid.toZPow Group.toDivInvMonoid SeminormedGroup.toGroup SeminormedCommGroup.toSeminormedGroup Real.instMul NormedAddCommGroup.toNorm Int.instNormedAddCommGroup	—	zpow_natCast Int.norm_natCast norm_pow_le_mul_norm zpow_neg norm_inv' norm_neg
norm_zsmul_le 📖	mathematical	—	Real Real.instLE Norm.norm SeminormedAddCommGroup.toNorm SubNegMonoid.toZSMul AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup Real.instMul NormedAddCommGroup.toNorm Int.instNormedAddCommGroup	—	natCast_zsmul Int.norm_natCast norm_nsmul_le neg_zsmul norm_neg

---

← Back to Index