Documentation Verification Report

Projection

📁 Source: Mathlib/Geometry/Euclidean/Angle/Unoriented/Projection.lean

Statistics

Metric	Count
Definitions	0
Theorems `angle_orthogonalProjection_self`, `angle_self_orthogonalProjection`	2
Total	2

EuclideanGeometry

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`angle_orthogonalProjection_self` 📖	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`	`angle` `AffineSubspace` `Real` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `Real.instRCLike` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NormedAddCommGroup.toSeminormedAddCommGroup` `InnerProductSpace.toNormedSpace` `NormedAddTorsor.toAddTorsor` `MetricSpace.toPseudoMetricSpace` `SetLike.instMembership` `AffineSubspace.instSetLike` `DFunLike.coe` `ContinuousAffineMap` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Submodule.setLike` `AffineSubspace.direction` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Submodule.addCommGroup` `Submodule.module` `instTopologicalSpaceSubtype` `AffineSubspace.toAddTorsor` `Real.instRing` `Real.normedField` `ContinuousAffineMap.instFunLike` `orthogonalProjection` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.pi` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	—	`Nat.instAtLeastTwoHAddOfNat` `angle_comm` `angle_self_orthogonalProjection`
`angle_self_orthogonalProjection` 📖	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`	`angle` `AffineSubspace` `Real` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `Real.instRCLike` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NormedAddCommGroup.toSeminormedAddCommGroup` `InnerProductSpace.toNormedSpace` `NormedAddTorsor.toAddTorsor` `MetricSpace.toPseudoMetricSpace` `SetLike.instMembership` `AffineSubspace.instSetLike` `DFunLike.coe` `ContinuousAffineMap` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Submodule.setLike` `AffineSubspace.direction` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Submodule.addCommGroup` `Submodule.module` `instTopologicalSpaceSubtype` `AffineSubspace.toAddTorsor` `Real.instRing` `Real.normedField` `ContinuousAffineMap.instFunLike` `orthogonalProjection` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.pi` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	—	`Nat.instAtLeastTwoHAddOfNat` `angle.eq_1` `InnerProductGeometry.inner_eq_zero_iff_angle_eq_pi_div_two` `Submodule.inner_left_of_mem_orthogonal` `AffineSubspace.vsub_mem_direction` `orthogonalProjection_mem` `vsub_orthogonalProjection_mem_direction_orthogonal`

---

← Back to Index