Documentation Verification Report

Reflection

📁 Source: Mathlib/Analysis/InnerProductSpace/Projection/Reflection.lean

Statistics

Metric	Count
Definitions `reflection`, `reflectionLinearEquiv`	2
Theorems `reflection_apply`, `reflection_bot`, `reflection_eq_self_iff`, `reflection_inv`, `reflection_involutive`, `reflection_map`, `reflection_map_apply`, `reflection_mem_subspace_eq_self`, `reflection_mem_subspace_orthogonalComplement_eq_neg`, `reflection_mem_subspace_orthogonal_precomplement_eq_neg`, `reflection_mul_reflection`, `reflection_orthogonal`, `reflection_orthogonalComplement_singleton_eq_neg`, `reflection_orthogonal_apply`, `reflection_reflection`, `reflection_singleton_apply`, `reflection_sub`, `reflection_symm`, `reflection_trans_reflection`	19
Total	21

Submodule

Definitions

Name	Category	Theorems
`reflection` 📖	CompOp	27 math math: `reflection_trans_reflection`, `reflection_orthogonal_apply`, `reflection_symm`, `reflection_singleton_apply`, `reflection_apply`, `reflection_orthogonalComplement_singleton_eq_neg`, `LinearIsometryEquiv.reflections_generate_dim_aux`, `LinearIsometryEquiv.reflections_generate`, `linearEquiv_det_reflection`, `reflection_mem_subspace_orthogonal_precomplement_eq_neg`, `reflection_reflection`, `EuclideanGeometry.reflection_apply_of_mem`, `reflection_inv`, `reflection_mul_reflection`, `reflection_sub`, `reflection_map`, `det_reflection`, `reflection_orthogonal`, `reflection_eq_self_iff`, `reflection_bot`, `reflection_map_apply`, `EuclideanGeometry.hasFDerivAt_inversion`, `reflection_involutive`, `LinearIsometryEquiv.reflections_generate_dim`, `reflection_mem_subspace_eq_self`, `EuclideanGeometry.reflection_apply`, `reflection_mem_subspace_orthogonalComplement_eq_neg`
`reflectionLinearEquiv` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`reflection_apply` 📖	mathematical	—	`DFunLike.coe` `LinearIsometryEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `EquivLike.toFunLike` `LinearIsometryEquiv.instEquivLike` `reflection` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `AddMonoid.toNatSMul` `ESeminormedAddMonoid.toAddMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `ContinuousLinearMap` `ESeminormedAddCommMonoid.toAddCommMonoid` `ContinuousLinearMap.funLike` `starProjection`	—	`RingHomInvPair.ids`
`reflection_bot` 📖	mathematical	—	`reflection` `Bot.bot` `Submodule` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `instBot` `HasOrthogonalProjection.ofCompleteSpace` `complete_of_proper` `SetLike.instMembership` `setLike` `Subtype.pseudoMetricSpace` `FiniteDimensional.RCLike.properSpace_submodule` `finiteDimensional_bot` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `SeminormedAddCommGroup.toAddCommGroup` `LinearIsometryEquiv.neg`	—	`LinearIsometryEquiv.ext` `RingHomInvPair.ids` `HasOrthogonalProjection.ofCompleteSpace` `complete_of_proper` `FiniteDimensional.RCLike.properSpace_submodule` `finiteDimensional_bot` `starProjection_bot` `nsmul_zero` `zero_sub`
`reflection_eq_self_iff` 📖	mathematical	—	`DFunLike.coe` `LinearIsometryEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `EquivLike.toFunLike` `LinearIsometryEquiv.instEquivLike` `reflection` `Submodule` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `SetLike.instMembership` `setLike`	—	`RingHomInvPair.ids` `starProjection_eq_self_iff` `reflection_apply` `sub_eq_iff_eq_add'` `Nat.instAtLeastTwoHAddOfNat` `two_smul` `smul_right_injective` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `instIsDomain` `GroupWithZero.toNoZeroSMulDivisors` `IsDomain.toIsCancelMulZero` `two_ne_zero` `CharZero.NeZero.two` `RCLike.charZero_rclike`
`reflection_inv` 📖	mathematical	—	`LinearIsometryEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `LinearIsometryEquiv.instGroup` `reflection`	—	`RingHomInvPair.ids`
`reflection_involutive` 📖	mathematical	—	`Function.Involutive` `DFunLike.coe` `LinearIsometryEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `EquivLike.toFunLike` `LinearIsometryEquiv.instEquivLike` `reflection`	—	`reflection_reflection`
`reflection_map` 📖	mathematical	—	`reflection` `map` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomSurjective.ids` `LinearEquiv.toLinearMap` `RingHomInvPair.ids` `LinearIsometryEquiv.toLinearEquiv` `HasOrthogonalProjection.map_linearIsometryEquiv` `LinearIsometryEquiv.trans` `RingHomCompTriple.ids` `LinearIsometryEquiv.symm`	—	`RingHomInvPair.ids` `LinearIsometryEquiv.ext` `RingHomSurjective.ids` `HasOrthogonalProjection.map_linearIsometryEquiv` `RingHomCompTriple.ids` `reflection_map_apply`
`reflection_map_apply` 📖	mathematical	—	`DFunLike.coe` `LinearIsometryEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `EquivLike.toFunLike` `LinearIsometryEquiv.instEquivLike` `reflection` `map` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `RingHomSurjective.ids` `LinearEquiv.toLinearMap` `LinearIsometryEquiv.toLinearEquiv` `HasOrthogonalProjection.map_linearIsometryEquiv` `LinearIsometryEquiv.symm`	—	`RingHomInvPair.ids` `RingHomSurjective.ids` `HasOrthogonalProjection.map_linearIsometryEquiv` `starProjection_map_apply` `two_smul` `map_sub` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `SemilinearIsometryClass.toSemilinearMapClass` `SemilinearIsometryEquivClass.toSemilinearIsometryClass` `LinearIsometryEquiv.instSemilinearIsometryEquivClass` `map_add` `SemilinearMapClass.toAddHomClass` `LinearIsometryEquiv.apply_symm_apply`
`reflection_mem_subspace_eq_self` 📖	mathematical	`Submodule` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `SetLike.instMembership` `setLike`	`DFunLike.coe` `LinearIsometryEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `EquivLike.toFunLike` `LinearIsometryEquiv.instEquivLike` `reflection`	—	`RingHomInvPair.ids` `reflection_eq_self_iff`
`reflection_mem_subspace_orthogonalComplement_eq_neg` 📖	mathematical	`Submodule` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `SetLike.instMembership` `setLike` `orthogonal`	`DFunLike.coe` `LinearIsometryEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `EquivLike.toFunLike` `LinearIsometryEquiv.instEquivLike` `reflection` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	—	`RingHomInvPair.ids` `orthogonalProjection_mem_subspace_orthogonalComplement_eq_zero` `nsmul_zero` `zero_sub`
`reflection_mem_subspace_orthogonal_precomplement_eq_neg` 📖	mathematical	`Submodule` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `SetLike.instMembership` `setLike`	`DFunLike.coe` `LinearIsometryEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `EquivLike.toFunLike` `LinearIsometryEquiv.instEquivLike` `reflection` `orthogonal` `instHasOrthogonalProjectionOrthogonal` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	—	`reflection_mem_subspace_orthogonalComplement_eq_neg` `instHasOrthogonalProjectionOrthogonal` `le_orthogonal_orthogonal`
`reflection_mul_reflection` 📖	mathematical	—	`LinearIsometryEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `LinearIsometryEquiv.instGroup` `reflection` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`reflection_trans_reflection`
`reflection_orthogonal` 📖	mathematical	—	`reflection` `orthogonal` `instHasOrthogonalProjectionOrthogonal` `LinearIsometryEquiv.trans` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `RingHomCompTriple.ids` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `LinearIsometryEquiv.neg`	—	`LinearIsometryEquiv.ext` `RingHomInvPair.ids` `instHasOrthogonalProjectionOrthogonal` `RingHomCompTriple.ids` `reflection_orthogonal_apply`
`reflection_orthogonalComplement_singleton_eq_neg` 📖	mathematical	—	`DFunLike.coe` `LinearIsometryEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `EquivLike.toFunLike` `LinearIsometryEquiv.instEquivLike` `reflection` `orthogonal` `span` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Set` `Set.instSingletonSet` `instHasOrthogonalProjectionOrthogonal` `HasOrthogonalProjection.ofCompleteSpace` `complete_of_proper` `Submodule` `SetLike.instMembership` `setLike` `Subtype.pseudoMetricSpace` `FiniteDimensional.RCLike.properSpace_submodule` `FiniteDimensional.span_singleton` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `SeminormedAddCommGroup.toAddCommGroup` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	—	`reflection_mem_subspace_orthogonal_precomplement_eq_neg` `HasOrthogonalProjection.ofCompleteSpace` `complete_of_proper` `FiniteDimensional.RCLike.properSpace_submodule` `FiniteDimensional.span_singleton` `mem_span_singleton_self`
`reflection_orthogonal_apply` 📖	mathematical	—	`DFunLike.coe` `LinearIsometryEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `EquivLike.toFunLike` `LinearIsometryEquiv.instEquivLike` `reflection` `orthogonal` `instHasOrthogonalProjectionOrthogonal` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	—	`RingHomInvPair.ids` `instHasOrthogonalProjectionOrthogonal` `starProjection_orthogonal_val` `neg_sub` `Mathlib.Tactic.Abel.unfold_sub` `Mathlib.Tactic.Abel.subst_into_addg` `Mathlib.Tactic.Abel.subst_into_smul_upcast` `Mathlib.Tactic.Abel.term_atomg` `Mathlib.Tactic.Abel.subst_into_negg` `Mathlib.Tactic.Abel.term_neg` `neg_zero` `Mathlib.Tactic.Abel.term_add_constg` `zero_add` `Mathlib.Tactic.Abel.term_smulg` `Mathlib.Meta.NormNum.IsNat.to_eq` `Mathlib.Meta.NormNum.isNat_mul` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.IsInt.neg_to_eq` `Mathlib.Meta.NormNum.isInt_mul` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.isInt_neg` `Mathlib.Tactic.Abel.zero_smulg` `Mathlib.Tactic.Abel.term_add_termg` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `add_zero`
`reflection_reflection` 📖	mathematical	—	`DFunLike.coe` `LinearIsometryEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `EquivLike.toFunLike` `LinearIsometryEquiv.instEquivLike` `reflection`	—	`LinearEquiv.left_inv` `RingHomInvPair.ids`
`reflection_singleton_apply` 📖	mathematical	—	`DFunLike.coe` `LinearIsometryEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `EquivLike.toFunLike` `LinearIsometryEquiv.instEquivLike` `reflection` `span` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Set` `Set.instSingletonSet` `HasOrthogonalProjection.ofCompleteSpace` `complete_of_proper` `Submodule` `SetLike.instMembership` `setLike` `Subtype.pseudoMetricSpace` `FiniteDimensional.RCLike.properSpace_submodule` `FiniteDimensional.span_singleton` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `SeminormedAddCommGroup.toAddCommGroup` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `AddMonoid.toNatSMul` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `DivInvMonoid.toDiv` `DivisionRing.toDivInvMonoid` `Inner.inner` `InnerProductSpace.toInner` `Monoid.toNatPow` `RCLike.ofReal` `Norm.norm` `NormedAddCommGroup.toNorm`	—	`RingHomInvPair.ids` `HasOrthogonalProjection.ofCompleteSpace` `complete_of_proper` `FiniteDimensional.RCLike.properSpace_submodule` `FiniteDimensional.span_singleton` `reflection_apply` `starProjection_singleton` `RCLike.ofReal_pow`
`reflection_sub` 📖	mathematical	`Norm.norm` `NormedAddCommGroup.toNorm`	`DFunLike.coe` `LinearIsometryEquiv` `Real` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `Real.instRCLike` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `EquivLike.toFunLike` `LinearIsometryEquiv.instEquivLike` `reflection` `orthogonal` `span` `Real.semiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Set` `Set.instSingletonSet` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `instHasOrthogonalProjectionOrthogonal` `HasOrthogonalProjection.ofCompleteSpace` `complete_of_proper` `Submodule` `SetLike.instMembership` `setLike` `Subtype.pseudoMetricSpace` `FiniteDimensional.RCLike.properSpace_submodule` `FiniteDimensional.span_singleton` `Real.instDivisionRing` `SeminormedAddCommGroup.toAddCommGroup`	—	`RingHomInvPair.ids` `instHasOrthogonalProjectionOrthogonal` `HasOrthogonalProjection.ofCompleteSpace` `complete_of_proper` `FiniteDimensional.RCLike.properSpace_submodule` `FiniteDimensional.span_singleton` `reflection_orthogonalComplement_singleton_eq_neg` `reflection_mem_subspace_eq_self` `mem_orthogonal_singleton_iff_inner_left` `real_inner_add_sub_eq_zero_iff` `map_add` `SemilinearMapClass.toAddHomClass` `SemilinearIsometryClass.toSemilinearMapClass` `SemilinearIsometryEquivClass.toSemilinearIsometryClass` `LinearIsometryEquiv.instSemilinearIsometryEquivClass` `map_sub` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `add_add_sub_cancel` `Mathlib.Tactic.Abel.subst_into_addg` `Mathlib.Tactic.Abel.term_atomg` `Mathlib.Tactic.Abel.term_add_termg` `Mathlib.Meta.NormNum.IsNat.to_eq` `Mathlib.Meta.NormNum.isNat_add` `Mathlib.Meta.NormNum.isNat_ofNat` `zero_add` `Mathlib.Tactic.Abel.const_add_termg` `add_zero` `Mathlib.Tactic.Abel.subst_into_negg` `Mathlib.Tactic.Abel.unfold_sub` `Mathlib.Tactic.Abel.term_neg` `neg_zero` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_neg` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Abel.zero_termg` `smul_right_injective` `Nat.instAtLeastTwoHAddOfNat` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `Real.instIsDomain` `GroupWithZero.toNoZeroSMulDivisors` `IsDomain.toIsCancelMulZero` `RCLike.charZero_rclike` `two_smul`
`reflection_symm` 📖	mathematical	—	`LinearIsometryEquiv.symm` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `reflection`	—	`RingHomInvPair.ids`
`reflection_trans_reflection` 📖	mathematical	—	`LinearIsometryEquiv.trans` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `RingHomCompTriple.ids` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `reflection` `LinearIsometryEquiv.refl`	—	`LinearIsometryEquiv.ext` `RingHomInvPair.ids` `RingHomCompTriple.ids` `reflection_involutive`

---

← Back to Index