Projection

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

Statistics

Metric	Count
Definitions	0
Theorems oangle_orthogonalProjection_self, oangle_self_orthogonalProjection, two_zsmul_oangle_orthogonalProjection_self, two_zsmul_oangle_self_orthogonalProjection	4
Total	4

EuclideanGeometry

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
oangle_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	oangle NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField DFunLike.coe ContinuousAffineMap Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Submodule.setLike AffineSubspace.direction UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Submodule.addCommGroup SeminormedAddCommGroup.toAddCommGroup Submodule.module instTopologicalSpaceSubtype AffineSubspace.toAddTorsor ContinuousAffineMap.instFunLike orthogonalProjection Real.Angle.coe DivInvMonoid.toDiv Real.instDivInvMonoid Real.pi instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Real.instNeg	—	Real.instIsStrictOrderedRing Nat.instAtLeastTwoHAddOfNat oangle_rev neg_eq_iff_eq_neg Real.Angle.coe_neg neg_div neg_neg oangle_self_orthogonalProjection
oangle_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	oangle NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField DFunLike.coe ContinuousAffineMap Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Submodule.setLike AffineSubspace.direction UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Submodule.addCommGroup SeminormedAddCommGroup.toAddCommGroup Submodule.module instTopologicalSpaceSubtype AffineSubspace.toAddTorsor ContinuousAffineMap.instFunLike orthogonalProjection Real.Angle.coe DivInvMonoid.toDiv Real.instDivInvMonoid Real.pi instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Real.instNeg	—	Real.instIsStrictOrderedRing Iff.not orthogonalProjection_eq_self_iff oangle_eq_angle_or_eq_neg_angle Nat.instAtLeastTwoHAddOfNat neg_div angle_self_orthogonalProjection
two_zsmul_oangle_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	Real.Angle SubNegMonoid.toZSMul AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup Real.instNormedAddCommGroupAngle oangle NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField DFunLike.coe ContinuousAffineMap Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Submodule.setLike AffineSubspace.direction UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Submodule.addCommGroup SeminormedAddCommGroup.toAddCommGroup Submodule.module instTopologicalSpaceSubtype AffineSubspace.toAddTorsor ContinuousAffineMap.instFunLike orthogonalProjection Real.Angle.coe Real.pi	—	Real.instIsStrictOrderedRing Nat.instAtLeastTwoHAddOfNat Real.Angle.two_zsmul_eq_pi_iff oangle_orthogonalProjection_self
two_zsmul_oangle_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	Real.Angle SubNegMonoid.toZSMul AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup Real.instNormedAddCommGroupAngle oangle NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField DFunLike.coe ContinuousAffineMap Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Submodule.setLike AffineSubspace.direction UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Submodule.addCommGroup SeminormedAddCommGroup.toAddCommGroup Submodule.module instTopologicalSpaceSubtype AffineSubspace.toAddTorsor ContinuousAffineMap.instFunLike orthogonalProjection Real.Angle.coe Real.pi	—	Real.instIsStrictOrderedRing Nat.instAtLeastTwoHAddOfNat Real.Angle.two_zsmul_eq_pi_iff oangle_self_orthogonalProjection

---

← Back to Index