Documentation Verification Report

Power

📁 Source: Mathlib/Geometry/Euclidean/Sphere/Power.lean

Statistics

Metric	Count
Definitions `power`	1
Theorems `power_eq_dist_sq`, `dist_sq_eq_mul_dist_of_tangent_and_secant`, `isTangentAt_iff_dist_sq_eq_power`, `isTangentAt_of_dist_sq_eq_power`, `mul_dist_eq_abs_power`, `mul_dist_eq_neg_power_of_dist_center_le_radius`, `mul_dist_eq_power_of_radius_le_dist_center`, `mul_dist_eq_zero_of_mem_sphere`, `power_eq_zero_iff_mem_sphere`, `power_neg_iff_dist_center_lt_radius`, `power_nonneg_iff_radius_le_dist_center`, `power_nonpos_iff_dist_center_le_radius`, `power_pos_iff_radius_lt_dist_center`, `mul_dist_eq_abs_sub_sq_dist`, `mul_dist_eq_mul_dist_of_cospherical`, `mul_dist_eq_mul_dist_of_cospherical_of_angle_eq_pi`, `mul_dist_eq_mul_dist_of_cospherical_of_angle_eq_zero`, `mul_norm_eq_abs_sub_sq_norm`	18
Total	19

EuclideanGeometry

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mul_dist_eq_abs_sub_sq_dist` 📖	mathematical	`AffineSubspace` `Real` `Real.instRing` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddTorsor.toAddTorsor` `MetricSpace.toPseudoMetricSpace` `SetLike.instMembership` `AffineSubspace.instSetLike` `affineSpan` `Set` `Set.instInsert` `Set.instSingletonSet` `Dist.dist` `PseudoMetricSpace.toDist`	`Real.instMul` `abs` `Real.lattice` `Real.instAddGroup` `Real.instSub` `Monoid.toNatPow` `Real.instMonoid`	—	`RCLike.charZero_rclike` `vsub_sub_vsub_cancel_left` `Nat.instAtLeastTwoHAddOfNat` `midpoint_vsub_left` `right_vsub_midpoint` `add_comm` `vsub_add_vsub_cancel` `dist_eq_norm_vsub` `InnerProductGeometry.mul_norm_eq_abs_sub_sq_norm` `vadd_left_mem_affineSpan_pair` `vsub_vadd` `eq_sub_iff_add_eq'` `eq_sub_iff_add_eq` `Mathlib.Tactic.Module.NF.eq_of_eval_eq_eval` `Mathlib.Tactic.Module.NF.sub_eq_eval` `Mathlib.Tactic.Module.NF.atom_eq_eval` `Mathlib.Tactic.Module.NF.smul_eq_eval` `Mathlib.Tactic.Module.NF.add_eq_eval` `Mathlib.Tactic.Module.NF.add_eq_eval₂` `zero_add` `Mathlib.Tactic.Module.NF.eval_algebraMap` `AddCommMonoid.nat_isScalarTower` `AddCommGroup.intIsScalarTower` `Mathlib.Tactic.Module.NF.sub_eq_eval₂` `Mathlib.Tactic.Module.NF.zero_sub_eq_eval` `Mathlib.Tactic.Module.NF.eq_cons_cons` `eq_natCast` `RingHom.instRingHomClass` `Nat.cast_one` `eq_intCast` `Int.cast_one` `Nat.cast_add` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.add_pf_add_overlap` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.isNat_add` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_add` `Mathlib.Tactic.Ring.neg_mul` `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.Tactic.Ring.neg_zero` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Meta.NormNum.instAtLeastTwo` `Mathlib.Tactic.Ring.mul_one`
`mul_dist_eq_mul_dist_of_cospherical` 📖	mathematical	`Cospherical` `Set` `Set.instInsert` `Set.instSingletonSet` `AffineSubspace` `Real` `Real.instRing` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddTorsor.toAddTorsor` `MetricSpace.toPseudoMetricSpace` `SetLike.instMembership` `AffineSubspace.instSetLike` `affineSpan`	`Real.instMul` `Dist.dist` `PseudoMetricSpace.toDist`	—	`cospherical_def` `mul_dist_eq_abs_sub_sq_dist`
`mul_dist_eq_mul_dist_of_cospherical_of_angle_eq_pi` 📖	mathematical	`Cospherical` `Set` `Set.instInsert` `Set.instSingletonSet` `angle` `Real.pi`	`Real` `Real.instMul` `Dist.dist` `PseudoMetricSpace.toDist` `MetricSpace.toPseudoMetricSpace`	—	`mul_dist_eq_mul_dist_of_cospherical` `Wbtw.mem_affineSpan` `Sbtw.wbtw` `angle_eq_pi_iff_sbtw`
`mul_dist_eq_mul_dist_of_cospherical_of_angle_eq_zero` 📖	mathematical	`Cospherical` `Set` `Set.instInsert` `Set.instSingletonSet` `angle` `Real` `Real.instZero`	`Real.instMul` `Dist.dist` `PseudoMetricSpace.toDist` `MetricSpace.toPseudoMetricSpace`	—	`mul_dist_eq_mul_dist_of_cospherical` `Collinear.mem_affineSpan_of_mem_of_ne` `collinear_of_angle_eq_zero`

EuclideanGeometry.Sphere

Definitions

Name	Category	Theorems
`power` 📖	CompOp	10 math math: `mul_dist_eq_abs_power`, `mul_dist_eq_neg_power_of_dist_center_le_radius`, `power_pos_iff_radius_lt_dist_center`, `IsTangentAt.power_eq_dist_sq`, `power_neg_iff_dist_center_lt_radius`, `power_eq_zero_iff_mem_sphere`, `mul_dist_eq_power_of_radius_le_dist_center`, `power_nonneg_iff_radius_le_dist_center`, `power_nonpos_iff_dist_center_le_radius`, `isTangentAt_iff_dist_sq_eq_power`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`dist_sq_eq_mul_dist_of_tangent_and_secant` 📖	mathematical	`EuclideanGeometry.Sphere` `EuclideanGeometry.instMembershipSphere` `AffineSubspace` `Real` `Real.instRing` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddTorsor.toAddTorsor` `MetricSpace.toPseudoMetricSpace` `SetLike.instMembership` `AffineSubspace.instSetLike` `affineSpan` `Set` `Set.instInsert` `Set.instSingletonSet` `IsTangentAt`	`Monoid.toNatPow` `Real.instMonoid` `Dist.dist` `PseudoMetricSpace.toDist` `Real.instMul`	—	`radius_nonneg_of_mem` `IsTangent.radius_le_dist_center` `IsTangentAt.isTangent` `left_mem_affineSpan_pair` `mul_dist_eq_power_of_radius_le_dist_center` `power.eq_1` `IsTangentAt.dist_sq_eq_of_mem` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.pow_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Tactic.Ring.pow_add` `Mathlib.Tactic.Ring.single_pow` `Mathlib.Tactic.Ring.mul_pow` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.one_pow` `Mathlib.Tactic.Ring.pow_zero` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_add` `Mathlib.Tactic.Ring.neg_mul` `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.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.add_pf_zero_add`
`isTangentAt_iff_dist_sq_eq_power` 📖	mathematical	`EuclideanGeometry.Sphere` `EuclideanGeometry.instMembershipSphere`	`IsTangentAt` `affineSpan` `Real` `Real.instRing` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddTorsor.toAddTorsor` `MetricSpace.toPseudoMetricSpace` `Set` `Set.instInsert` `Set.instSingletonSet` `Monoid.toNatPow` `Real.instMonoid` `Dist.dist` `PseudoMetricSpace.toDist` `power`	—	`IsTangentAt.power_eq_dist_sq` `norm_add_sq_eq_norm_sq_add_norm_sq_iff_real_inner_eq_zero` `Mathlib.Tactic.Linarith.eq_of_not_lt_of_not_gt` `Mathlib.Tactic.Linarith.lt_irrefl` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pp_pf_overlap` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.isNat_add` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_add` `Mathlib.Tactic.Ring.neg_mul` `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.Tactic.Ring.neg_zero` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.cast_zero` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_zero` `Mathlib.Tactic.Linarith.lt_of_eq_of_lt` `sub_eq_zero_of_eq` `dist_eq_norm_vsub` `sq` `vsub_add_vsub_cancel` `EuclideanGeometry.mem_sphere` `Mathlib.Tactic.Linarith.sub_neg_of_lt` `Real.instIsOrderedRing` `Mathlib.Tactic.Ring.neg_congr` `neg_eq_zero` `right_mem_affineSpan_pair` `mem_orthRadius_iff_inner_left` `vadd_right_mem_affineSpan_pair` `vsub_vadd` `inner_smul_left` `MulZeroClass.mul_zero`
`isTangentAt_of_dist_sq_eq_power` 📖	mathematical	`EuclideanGeometry.Sphere` `EuclideanGeometry.instMembershipSphere` `Real` `Monoid.toNatPow` `Real.instMonoid` `Dist.dist` `PseudoMetricSpace.toDist` `MetricSpace.toPseudoMetricSpace` `power`	`IsTangentAt` `affineSpan` `Real.instRing` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddTorsor.toAddTorsor` `Set` `Set.instInsert` `Set.instSingletonSet`	—	`isTangentAt_iff_dist_sq_eq_power`
`mul_dist_eq_abs_power` 📖	mathematical	`AffineSubspace` `Real` `Real.instRing` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddTorsor.toAddTorsor` `MetricSpace.toPseudoMetricSpace` `SetLike.instMembership` `AffineSubspace.instSetLike` `affineSpan` `Set` `Set.instInsert` `Set.instSingletonSet` `EuclideanGeometry.Sphere` `EuclideanGeometry.instMembershipSphere`	`Real.instMul` `Dist.dist` `PseudoMetricSpace.toDist` `abs` `Real.lattice` `Real.instAddGroup` `power`	—	`EuclideanGeometry.mem_sphere` `dist_comm` `EuclideanGeometry.mul_dist_eq_abs_sub_sq_dist` `power.eq_1` `abs_sub_comm`
`mul_dist_eq_neg_power_of_dist_center_le_radius` 📖	mathematical	`Real` `Real.instLE` `Real.instZero` `radius` `AffineSubspace` `Real.instRing` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddTorsor.toAddTorsor` `MetricSpace.toPseudoMetricSpace` `SetLike.instMembership` `AffineSubspace.instSetLike` `affineSpan` `Set` `Set.instInsert` `Set.instSingletonSet` `EuclideanGeometry.Sphere` `EuclideanGeometry.instMembershipSphere` `Dist.dist` `PseudoMetricSpace.toDist` `center`	`Real.instMul` `Real.instNeg` `power`	—	`mul_dist_eq_abs_power` `abs_of_nonpos` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `power_nonpos_iff_dist_center_le_radius`
`mul_dist_eq_power_of_radius_le_dist_center` 📖	mathematical	`Real` `Real.instLE` `Real.instZero` `radius` `AffineSubspace` `Real.instRing` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddTorsor.toAddTorsor` `MetricSpace.toPseudoMetricSpace` `SetLike.instMembership` `AffineSubspace.instSetLike` `affineSpan` `Set` `Set.instInsert` `Set.instSingletonSet` `EuclideanGeometry.Sphere` `EuclideanGeometry.instMembershipSphere` `Dist.dist` `PseudoMetricSpace.toDist` `center`	`Real.instMul` `power`	—	`mul_dist_eq_abs_power` `abs_of_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `power_nonneg_iff_radius_le_dist_center`
`mul_dist_eq_zero_of_mem_sphere` 📖	mathematical	`AffineSubspace` `Real` `Real.instRing` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddTorsor.toAddTorsor` `MetricSpace.toPseudoMetricSpace` `SetLike.instMembership` `AffineSubspace.instSetLike` `affineSpan` `Set` `Set.instInsert` `Set.instSingletonSet` `EuclideanGeometry.Sphere` `EuclideanGeometry.instMembershipSphere`	`Real.instMul` `Dist.dist` `PseudoMetricSpace.toDist` `Real.instZero`	—	`EuclideanGeometry.mem_sphere` `dist_comm` `EuclideanGeometry.mul_dist_eq_abs_sub_sq_dist` `sub_self` `abs_zero` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid`
`power_eq_zero_iff_mem_sphere` 📖	mathematical	`Real` `Real.instLE` `Real.instZero` `radius`	`power` `EuclideanGeometry.Sphere` `EuclideanGeometry.instMembershipSphere`	—	`power.eq_1` `EuclideanGeometry.mem_sphere` `sub_eq_zero` `pow_left_inj₀` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `IsOrderedRing.toMulPosMono` `Real.instIsOrderedRing` `dist_nonneg` `two_ne_zero`
`power_neg_iff_dist_center_lt_radius` 📖	mathematical	`Real` `Real.instLE` `Real.instZero` `radius`	`Real.instLT` `power` `Dist.dist` `PseudoMetricSpace.toDist` `MetricSpace.toPseudoMetricSpace` `center`	—	`power.eq_1` `sub_neg` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `pow_lt_pow_iff_left₀` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `IsOrderedRing.toMulPosMono` `Real.instIsOrderedRing` `dist_nonneg` `two_ne_zero`
`power_nonneg_iff_radius_le_dist_center` 📖	mathematical	`Real` `Real.instLE` `Real.instZero` `radius`	`power` `Dist.dist` `PseudoMetricSpace.toDist` `MetricSpace.toPseudoMetricSpace` `center`	—	`power.eq_1` `sub_nonneg` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `pow_le_pow_iff_left₀` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `IsOrderedRing.toMulPosMono` `Real.instIsOrderedRing` `dist_nonneg` `two_ne_zero`
`power_nonpos_iff_dist_center_le_radius` 📖	mathematical	`Real` `Real.instLE` `Real.instZero` `radius`	`power` `Dist.dist` `PseudoMetricSpace.toDist` `MetricSpace.toPseudoMetricSpace` `center`	—	`power.eq_1` `sub_nonpos` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `pow_le_pow_iff_left₀` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `IsOrderedRing.toMulPosMono` `Real.instIsOrderedRing` `dist_nonneg` `two_ne_zero`
`power_pos_iff_radius_lt_dist_center` 📖	mathematical	`Real` `Real.instLE` `Real.instZero` `radius`	`Real.instLT` `power` `Dist.dist` `PseudoMetricSpace.toDist` `MetricSpace.toPseudoMetricSpace` `center`	—	`power.eq_1` `sub_pos` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `pow_lt_pow_iff_left₀` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `IsOrderedRing.toMulPosMono` `Real.instIsOrderedRing` `dist_nonneg` `two_ne_zero`

EuclideanGeometry.Sphere.IsTangentAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`power_eq_dist_sq` 📖	mathematical	`EuclideanGeometry.Sphere.IsTangentAt` `affineSpan` `Real` `Real.instRing` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddTorsor.toAddTorsor` `MetricSpace.toPseudoMetricSpace` `Set` `Set.instInsert` `Set.instSingletonSet`	`EuclideanGeometry.Sphere.power` `Monoid.toNatPow` `Real.instMonoid` `Dist.dist` `PseudoMetricSpace.toDist`	—	`EuclideanGeometry.Sphere.power.eq_1` `dist_sq_eq_of_mem` `left_mem_affineSpan_pair` `Nat.instAtLeastTwoHAddOfNat` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.pow_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Tactic.Ring.pow_add` `Mathlib.Tactic.Ring.single_pow` `Mathlib.Tactic.Ring.mul_pow` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.one_pow` `Mathlib.Tactic.Ring.pow_zero` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_add` `Mathlib.Tactic.Ring.neg_mul` `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.add_pf_add_overlap_zero` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.RingNF.nat_rawCast_1` `mul_one` `add_zero`

InnerProductGeometry

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mul_norm_eq_abs_sub_sq_norm` 📖	mathematical	`Real` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `Real.semiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `NormedSpace.toModule` `Real.normedField` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `Norm.norm` `NormedAddCommGroup.toNorm` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	`Real.instMul` `abs` `Real.lattice` `Real.instAddGroup` `Real.instSub` `Monoid.toNatPow`	—	`Nat.instAtLeastTwoHAddOfNat` `inner_eq_zero_iff_angle_eq_pi_div_two` `norm_add_eq_norm_sub_iff_angle_eq_pi_div_two` `inner_smul_right` `MulZeroClass.mul_zero` `sub_smul` `one_smul` `add_smul` `norm_smul` `NormedSpace.toNormSMulClass` `Mathlib.Tactic.Ring.of_eq` `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.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.mul_pp_pf_overlap` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.isNat_add` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.pow_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Tactic.Ring.pow_add` `Mathlib.Tactic.Ring.single_pow` `Mathlib.Tactic.Ring.mul_pow` `Mathlib.Tactic.Ring.one_pow` `Mathlib.Tactic.Ring.pow_zero` `abs_mul` `Real.instIsOrderedRing` `abs_pow` `abs_norm` `Mathlib.Tactic.Ring.sub_congr` `Nat.cast_one` `Mathlib.Tactic.Ring.sub_pf` `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.Tactic.Ring.neg_zero` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.mul_one` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.RingNF.nat_rawCast_1` `mul_one` `Mathlib.Tactic.RingNF.int_rawCast_neg` `Mathlib.Tactic.RingNF.mul_neg` `add_zero` `Mathlib.Tactic.RingNF.add_neg` `mul_pow` `sq_abs` `norm_add_sq_real` `norm_sub_sq_real` `sub_zero` `add_sub_add_left_eq_sub` `abs_sub_comm`

---

← Back to Index