Symmetric

📁 Source: Mathlib/Analysis/InnerProductSpace/Symmetric.lean

Statistics

Metric	Count
Definitions IsSymmetric, IsSymmetricProjection	2
Theorems isSymmetric_iff_orthogonal_range, isSymmetricProjection_rankOne_self, isSymmetric_rankOne_self, isSymmetric_symm_iff, isSymmetric_iff_isOrtho_range_ker, isSymmetric_iff_orthogonal_range, add, apply_clm, coe_reApplyInnerSelf_apply, coe_re_inner_apply_self, coe_re_inner_self_apply, conj_inner_sym, continuous, id, im_inner_apply_self, im_inner_self_apply, inner_map_polarization, inner_map_self_eq_zero, intCast, isSymmetric_smul_iff, mul_of_commute, natCast, orthogonal_range, pow, restrictScalars, restrict_invariant, smul, sub, toLinearMap_symm, zero, ext, ext_iff, isIdempotentElem, isSymmetric, sub_of_range_le_range, isSymmetricProjection_iff, isSymmetric_iff_inner_map_self_real, isSymmetric_iff_sesqForm, isSymmetric_linearIsometryEquiv_conj_iff, isSymmetric_sum, ker_le_ker_of_range, projection_isSymmetricProjection_iff, projection_isSymmetricProjection_of_isOrtho, projection_isSymmetric_iff	44
Total	46

ContinuousLinearMap.IsIdempotentElem

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isSymmetric_iff_orthogonal_range 📖	mathematical	IsIdempotentElem LinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RingHom.id Semiring.toNonAssocSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule InnerProductSpace.toNormedSpace Module.End.instMul	LinearMap.IsSymmetric Submodule.orthogonal LinearMap.range RingHomSurjective.ids LinearMap.ker	—	LinearMap.IsIdempotentElem.isSymmetric_iff_orthogonal_range

InnerProductSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isSymmetricProjection_rankOne_self 📖	mathematical	Norm.norm SeminormedAddCommGroup.toNorm Real Real.instOne	LinearMap.IsSymmetricProjection ContinuousLinearMap.toLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule toNormedSpace DFunLike.coe ContinuousLinearMap CommSemiring.toSemiring Semifield.toCommSemiring starRingEnd RCLike.toStarRing ContinuousLinearMap.topologicalSpace SeminormedAddCommGroup.toIsTopologicalAddGroup ContinuousLinearMap.addCommMonoid IsTopologicalAddGroup.toContinuousAdd SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup ContinuousLinearMap.module smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero IsBoundedSMul.toUniformContinuousConstSMul SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedSpace.toIsBoundedSMul ContinuousLinearMap.funLike ContinuousLinearMap.addCommGroup NormedRing.toRing NormedCommRing.toNormedRing ContinuousLinearMap.topologicalAddGroup ContinuousLinearMap.toSeminormedAddCommGroup DenselyNormedField.toNontriviallyNormedField RingHomIsometric.ids ContinuousLinearMap.smulCommClass ContinuousLinearMap.continuousConstSMul rankOne	—	SeminormedAddCommGroup.toIsTopologicalAddGroup IsTopologicalAddGroup.toContinuousAdd smulCommClass_self UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul ContinuousLinearMap.topologicalAddGroup RingHomIsometric.ids ContinuousLinearMap.smulCommClass ContinuousLinearMap.continuousConstSMul ContinuousLinearMap.IsIdempotentElem.toLinearMap isIdempotentElem_rankOne_self isSymmetric_rankOne_self
isSymmetric_rankOne_self 📖	mathematical	—	LinearMap.IsSymmetric ContinuousLinearMap.toLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule toNormedSpace DFunLike.coe ContinuousLinearMap CommSemiring.toSemiring Semifield.toCommSemiring starRingEnd RCLike.toStarRing ContinuousLinearMap.topologicalSpace SeminormedAddCommGroup.toIsTopologicalAddGroup ContinuousLinearMap.addCommMonoid IsTopologicalAddGroup.toContinuousAdd SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup ContinuousLinearMap.module smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero IsBoundedSMul.toUniformContinuousConstSMul SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedSpace.toIsBoundedSMul ContinuousLinearMap.funLike ContinuousLinearMap.addCommGroup NormedRing.toRing NormedCommRing.toNormedRing ContinuousLinearMap.topologicalAddGroup ContinuousLinearMap.toSeminormedAddCommGroup DenselyNormedField.toNontriviallyNormedField RingHomIsometric.ids ContinuousLinearMap.smulCommClass ContinuousLinearMap.continuousConstSMul rankOne	—	SeminormedAddCommGroup.toIsTopologicalAddGroup IsTopologicalAddGroup.toContinuousAdd smulCommClass_self UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul ContinuousLinearMap.topologicalAddGroup RingHomIsometric.ids ContinuousLinearMap.smulCommClass ContinuousLinearMap.continuousConstSMul inner_smul_left inner_conj_symm mul_comm inner_smul_right

LinearEquiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isSymmetric_symm_iff 📖	mathematical	—	LinearMap.IsSymmetric toLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule InnerProductSpace.toNormedSpace symm	—	RingHomInvPair.ids LinearMap.IsSymmetric.toLinearMap_symm

LinearMap

Definitions

Name	Category	Theorems
IsSymmetric 📖	MathDef	27 math math: ContinuousLinearMap.isSelfAdjoint_iff_isSymmetric, IsSelfAdjoint.isSymmetric, ContinuousLinearMap.isPositive_def, isSymmetric_adjoint_mul_self, ContinuousLinearMap.IsPositive.isSymmetric, IsSymmetricProjection.isSymmetric, isSymmetric_linearIsometryEquiv_conj_iff, ContinuousLinearMap.IsIdempotentElem.isSymmetric_iff_orthogonal_range, Submodule.starProjection_isSymmetric, IsIdempotentElem.isSymmetric_iff_isOrtho_range_ker, IsSymmetric.natCast, IsIdempotentElem.isSymmetric_iff_orthogonal_range, Matrix.isHermitian_iff_isSymmetric, IsPositive.isSymmetric, InnerProductSpace.isSymmetric_rankOne_self, isSymmetricProjection_iff, LinearEquiv.isSymmetric_symm_iff, IsSymmetric.zero, ContinuousLinearMap.isPositive_iff, IsSymmetric.id, isSymmetric_iff_isSelfAdjoint, isSymmetric_iff_sesqForm, isPositive_iff, isSymmetric_iff_inner_map_self_real, Submodule.IsCompl.projection_isSymmetric_iff, IsIdempotentElem.isPositive_iff_isSymmetric, IsSymmetric.intCast
IsSymmetricProjection 📖	CompData	10 math math: Submodule.IsCompl.projection_isSymmetricProjection_iff, ContinuousLinearMap.isStarProjection_iff_isSymmetricProjection, InnerProductSpace.isSymmetricProjection_rankOne_self, Submodule.IsCompl.projection_isSymmetricProjection_of_isOrtho, Submodule.isSymmetricProjection_starProjection, isSymmetricProjection_iff, isSymmetricProjection_iff_eq_coe_starProjection, isSymmetricProjection_iff_eq_coe_starProjection_range, ContinuousLinearMap.IsStarProjection.isSymmetricProjection, isStarProjection_iff_isSymmetricProjection

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isSymmetricProjection_iff 📖	mathematical	—	IsSymmetricProjection IsIdempotentElem LinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule InnerProductSpace.toNormedSpace Module.End.instMul IsSymmetric	—	—
isSymmetric_iff_inner_map_self_real 📖	mathematical	—	IsSymmetric Complex Complex.instRCLike DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring Complex.instCommSemiring RingHom.instFunLike starRingEnd Complex.instStarRing Inner.inner InnerProductSpace.toInner LinearMap Complex.instSemiring RingHom.id AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule Complex.instNormedField InnerProductSpace.toNormedSpace instFunLike	—	IsSymmetric.conj_inner_sym inner_conj_symm Nat.instAtLeastTwoHAddOfNat inner_map_polarization star_div₀ star_sub StarAddMonoid.star_add StarMul.star_mul Complex.conj_I inner_map_polarization' map_add SemilinearMapClass.toAddHomClass semilinearMapClass map_sub DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass map_smul SemilinearMapClass.toMulActionSemiHomClass mul_neg sub_neg_eq_add map_ofNat RingHom.instRingHomClass Mathlib.Meta.NormNum.isNat_eq_false Complex.instCharZero Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Nat.cast_zero Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.atom_pf 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_zero_add Mathlib.Tactic.Ring.mul_congr 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.neg_congr
isSymmetric_iff_sesqForm 📖	mathematical	—	IsSymmetric IsSelfAdjoint Semifield.toCommSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule InnerProductSpace.toNormedSpace ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedField.toNormedSpace starRingEnd RCLike.toStarRing flip CommSemiring.toSemiring Algebra.to_smulCommClass Algebra.id RingHom.id Semiring.toNonAssocSemiring innerₛₗ DFunLike.coe LinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring instFunLike	—	Algebra.to_smulCommClass
isSymmetric_linearIsometryEquiv_conj_iff 📖	mathematical	—	IsSymmetric comp DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule InnerProductSpace.toNormedSpace RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids LinearEquiv.toLinearMap RingHomInvPair.ids LinearIsometryEquiv.toLinearEquiv LinearIsometryEquiv.symm	—	RingHomInvPair.ids RingHomCompTriple.ids LinearIsometryEquiv.symm_apply_apply LinearIsometryEquiv.inner_map_eq_flip
isSymmetric_sum 📖	mathematical	IsSymmetric	Finset.sum LinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule InnerProductSpace.toNormedSpace addCommMonoid	—	coe_sum Finset.sum_apply sum_inner inner_sum Finset.sum_congr
ker_le_ker_of_range 📖	mathematical	IsSymmetric NormedAddCommGroup.toSeminormedAddCommGroup Submodule DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule InnerProductSpace.toNormedSpace Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder range RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids	ker	—	RingHomSurjective.ids mem_ker inner_self_eq_zero inner_zero_right

LinearMap.IsIdempotentElem

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isSymmetric_iff_isOrtho_range_ker 📖	mathematical	IsIdempotentElem LinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RingHom.id Semiring.toNonAssocSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule InnerProductSpace.toNormedSpace Module.End.instMul	LinearMap.IsSymmetric Submodule.IsOrtho LinearMap.range RingHomSurjective.ids LinearMap.ker	—	RingHomSurjective.ids LinearMap.IsProj.isCompl isProj_range Submodule.IsCompl.projection_isSymmetric_iff isCompl eq_isCompl_projection
isSymmetric_iff_orthogonal_range 📖	mathematical	IsIdempotentElem LinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RingHom.id Semiring.toNonAssocSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule InnerProductSpace.toNormedSpace Module.End.instMul	LinearMap.IsSymmetric Submodule.orthogonal LinearMap.range RingHomSurjective.ids LinearMap.ker	—	RingHomSurjective.ids LinearMap.IsSymmetric.orthogonal_range Submodule.isOrtho_orthogonal_right isSymmetric_iff_isOrtho_range_ker

LinearMap.IsSymmetric

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add 📖	mathematical	LinearMap.IsSymmetric	LinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule InnerProductSpace.toNormedSpace LinearMap.instAdd	—	LinearMap.add_apply inner_add_left inner_add_right
apply_clm 📖	mathematical	LinearMap.IsSymmetric ContinuousLinearMap.toLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule InnerProductSpace.toNormedSpace	Inner.inner InnerProductSpace.toInner DFunLike.coe ContinuousLinearMap ContinuousLinearMap.funLike	—	—
coe_reApplyInnerSelf_apply 📖	mathematical	LinearMap.IsSymmetric ContinuousLinearMap.toLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule InnerProductSpace.toNormedSpace	RCLike.ofReal ContinuousLinearMap.reApplyInnerSelf Inner.inner InnerProductSpace.toInner DFunLike.coe ContinuousLinearMap ContinuousLinearMap.funLike	—	RCLike.conj_eq_iff_real conj_inner_sym RCLike.ofReal_re
coe_re_inner_apply_self 📖	mathematical	LinearMap.IsSymmetric	RCLike.ofReal DFunLike.coe AddMonoidHom Real AddMonoid.toZero AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Ring.toSemiring CommRing.toRing Field.toCommRing NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField AddSemigroup.toAdd AddMonoid.toAddSemigroup AddZeroClass.toAddZero AddMonoid.toAddZeroClass Real.instAddMonoid AddMonoidHom.instFunLike RCLike.re Inner.inner InnerProductSpace.toInner LinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule InnerProductSpace.toNormedSpace LinearMap.instFunLike	—	RCLike.conj_eq_iff_re conj_inner_sym
coe_re_inner_self_apply 📖	mathematical	LinearMap.IsSymmetric	RCLike.ofReal DFunLike.coe AddMonoidHom Real AddMonoid.toZero AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Ring.toSemiring CommRing.toRing Field.toCommRing NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField AddSemigroup.toAdd AddMonoid.toAddSemigroup AddZeroClass.toAddZero AddMonoid.toAddZeroClass Real.instAddMonoid AddMonoidHom.instFunLike RCLike.re Inner.inner InnerProductSpace.toInner LinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule InnerProductSpace.toNormedSpace LinearMap.instFunLike	—	coe_re_inner_apply_self
conj_inner_sym 📖	mathematical	LinearMap.IsSymmetric	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring Semifield.toCommSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RingHom.instFunLike starRingEnd RCLike.toStarRing Inner.inner InnerProductSpace.toInner LinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring RingHom.id AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule InnerProductSpace.toNormedSpace LinearMap.instFunLike	—	inner_conj_symm
continuous 📖	mathematical	LinearMap.IsSymmetric NormedAddCommGroup.toSeminormedAddCommGroup	Continuous UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace DFunLike.coe LinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RingHom.id Semiring.toNonAssocSemiring ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule InnerProductSpace.toNormedSpace LinearMap.instFunLike	—	LinearMap.continuous_of_seq_closed_graph sub_eq_zero inner_self_eq_zero LinearMap.map_sub tendsto_nhds_unique TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace Filter.atTop_neBot instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat Filter.Tendsto.inner Filter.Tendsto.sub_const IsTopologicalAddGroup.to_continuousSub SeminormedAddCommGroup.toIsTopologicalAddGroup tendsto_const_nhds inner_zero_left sub_self
id 📖	mathematical	—	LinearMap.IsSymmetric LinearMap.id DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule InnerProductSpace.toNormedSpace	—	—
im_inner_apply_self 📖	mathematical	LinearMap.IsSymmetric	DFunLike.coe AddMonoidHom Real AddMonoid.toZero AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Ring.toSemiring CommRing.toRing Field.toCommRing NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField AddSemigroup.toAdd AddMonoid.toAddSemigroup AddZeroClass.toAddZero AddMonoid.toAddZeroClass Real.instAddMonoid AddMonoidHom.instFunLike RCLike.im Inner.inner InnerProductSpace.toInner LinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule InnerProductSpace.toNormedSpace LinearMap.instFunLike Real.instZero	—	RCLike.conj_eq_iff_im conj_inner_sym
im_inner_self_apply 📖	mathematical	LinearMap.IsSymmetric	DFunLike.coe AddMonoidHom Real AddMonoid.toZero AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Ring.toSemiring CommRing.toRing Field.toCommRing NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField AddSemigroup.toAdd AddMonoid.toAddSemigroup AddZeroClass.toAddZero AddMonoid.toAddZeroClass Real.instAddMonoid AddMonoidHom.instFunLike RCLike.im Inner.inner InnerProductSpace.toInner LinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule InnerProductSpace.toNormedSpace LinearMap.instFunLike Real.instZero	—	im_inner_apply_self
inner_map_polarization 📖	mathematical	LinearMap.IsSymmetric	Inner.inner InnerProductSpace.toInner DFunLike.coe LinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule InnerProductSpace.toNormedSpace LinearMap.instFunLike DivInvMonoid.toDiv DivisionRing.toDivInvMonoid NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup Distrib.toMul RCLike.I SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne NormedRing.toRing NormedCommRing.toNormedRing Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat RCLike.I_mul_I_ax MulZeroClass.zero_mul sub_zero add_zero map_add SemilinearMapClass.toAddHomClass LinearMap.semilinearMapClass map_sub DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass inner_add_left inner_add_right inner_sub_left inner_sub_right inner_conj_symm RCLike.re_add_im MulZeroClass.mul_zero Module.Free.instFaithfulSMulOfNontrivial Module.Free.of_divisionRing IsLocalRing.toNontrivial Field.instIsLocalRing RCLike.ofReal_re RCLike.conj_eq_iff_re Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.div_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.IsNat.of_raw 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.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.div_pf Mathlib.Tactic.Ring.inv_single Mathlib.Meta.NormNum.IsNNRat.to_raw_eq Mathlib.Meta.NormNum.isNNRat_inv_pos RCLike.charZero_rclike Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNNRat_mul Mathlib.Meta.NormNum.IsNNRat.of_raw Mathlib.Meta.NormNum.IsNNRat.den_nz Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.zero_mul map_smul SemilinearMapClass.toMulActionSemiHomClass inner_smul_left inner_smul_right RCLike.conj_I mul_add Distrib.leftDistribClass mul_sub sub_sub mul_neg neg_neg one_mul neg_one_mul Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.neg_congr
inner_map_self_eq_zero 📖	mathematical	LinearMap.IsSymmetric NormedAddCommGroup.toSeminormedAddCommGroup	Inner.inner InnerProductSpace.toInner DFunLike.coe LinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RingHom.id Semiring.toNonAssocSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule InnerProductSpace.toNormedSpace LinearMap.instFunLike MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing LinearMap.instZero	—	inner_self_eq_zero Nat.instAtLeastTwoHAddOfNat inner_map_polarization Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.div_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.cast_zero Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.div_pf Mathlib.Tactic.Ring.inv_single Mathlib.Meta.NormNum.IsNNRat.to_raw_eq Mathlib.Meta.NormNum.isNNRat_inv_pos RCLike.charZero_rclike Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.IsNat.of_raw inner_zero_left AddTorsor.nonempty
intCast 📖	mathematical	—	LinearMap.IsSymmetric LinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule InnerProductSpace.toNormedSpace AddGroupWithOne.toIntCast Ring.toAddGroupWithOne Module.End.instRing	—	Int.cast_smul_eq_zsmul inner_smul_left map_intCast RingHom.instRingHomClass inner_smul_right
isSymmetric_smul_iff 📖	mathematical	LinearMap.IsSymmetric NormedAddCommGroup.toSeminormedAddCommGroup	LinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RingHom.id Semiring.toNonAssocSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule InnerProductSpace.toNormedSpace LinearMap.instSMul DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid Module.toDistribMulAction smulCommClass_self CommRing.toCommMonoid EuclideanDomain.toCommRing Field.toEuclideanDomain DistribMulAction.toMulAction CommMonoid.toMonoid Ring.toSemiring CommRing.toRing IsSelfAdjoint InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing StarRing.toStarAddMonoid RCLike.toStarRing	—	smulCommClass_self inner_smul_left inner_smul_right IsCancelMulZero.toIsRightCancelMulZero IsDomain.toIsCancelMulZero instIsDomain ext_iff_inner_left inner_zero_right smul
mul_of_commute 📖	—	LinearMap.IsSymmetric Commute LinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule InnerProductSpace.toNormedSpace Module.End.instMul	—	—	Module.End.mul_apply
natCast 📖	mathematical	—	LinearMap.IsSymmetric LinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule InnerProductSpace.toNormedSpace AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Module.End.instRing	—	Nat.cast_smul_eq_nsmul inner_smul_left map_natCast RingHom.instRingHomClass inner_smul_right
orthogonal_range 📖	mathematical	LinearMap.IsSymmetric NormedAddCommGroup.toSeminormedAddCommGroup	Submodule.orthogonal LinearMap.range DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule InnerProductSpace.toNormedSpace RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids LinearMap.ker	—	Submodule.ext RingHomSurjective.ids inner_zero_right ext_inner_left
pow 📖	mathematical	LinearMap.IsSymmetric	LinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule InnerProductSpace.toNormedSpace Monoid.toNatPow Module.End.instMonoid	—	Nat.le_induction pow_zero RingHomCompTriple.ids Module.End.iterate_succ Module.End.mul_eq_comp mul_of_commute Commute.pow_left
restrictScalars 📖	mathematical	LinearMap.IsSymmetric	Real Real.instRCLike InnerProductSpace.rclikeToReal LinearMap.restrictScalars Real.semiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace LinearMap.IsScalarTower.compatibleSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Algebra.toSMul Semifield.toCommSemiring Ring.toSemiring SeminormedRing.toRing SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing NormedAlgebra.toAlgebra RCLike.toNormedAlgebra RestrictScalars.isScalarTower	—	LinearMap.IsScalarTower.compatibleSMul RestrictScalars.isScalarTower LinearMap.coe_restrictScalars
restrict_invariant 📖	mathematical	LinearMap.IsSymmetric Submodule DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule InnerProductSpace.toNormedSpace SetLike.instMembership Submodule.setLike DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike	Submodule.seminormedAddCommGroup NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing Submodule.innerProductSpace LinearMap.restrict	—	—
smul 📖	mathematical	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring Semifield.toCommSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RingHom.instFunLike starRingEnd RCLike.toStarRing LinearMap.IsSymmetric	LinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring RingHom.id AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule InnerProductSpace.toNormedSpace LinearMap.instSMul DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid Module.toDistribMulAction smulCommClass_self CommRing.toCommMonoid EuclideanDomain.toCommRing Field.toEuclideanDomain DistribMulAction.toMulAction CommMonoid.toMonoid Ring.toSemiring CommRing.toRing	—	smulCommClass_self inner_smul_left inner_smul_right
sub 📖	mathematical	LinearMap.IsSymmetric	LinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule InnerProductSpace.toNormedSpace LinearMap.instSub	—	LinearMap.sub_apply inner_sub_left inner_sub_right
toLinearMap_symm 📖	mathematical	LinearMap.IsSymmetric LinearEquiv.toLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule InnerProductSpace.toNormedSpace	LinearEquiv.symm	—	RingHomInvPair.ids LinearEquiv.apply_symm_apply
zero 📖	mathematical	—	LinearMap.IsSymmetric LinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule InnerProductSpace.toNormedSpace LinearMap.instZero	—	inner_zero_left inner_zero_right

LinearMap.IsSymmetricProjection

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ext 📖	—	LinearMap.IsSymmetricProjection NormedAddCommGroup.toSeminormedAddCommGroup LinearMap.range DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule InnerProductSpace.toNormedSpace RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids	—	—	RingHomSurjective.ids ext_iff
ext_iff 📖	mathematical	LinearMap.IsSymmetricProjection NormedAddCommGroup.toSeminormedAddCommGroup	LinearMap.range DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule InnerProductSpace.toNormedSpace RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids	—	RingHomSurjective.ids LinearMap.IsIdempotentElem.ext_iff isIdempotentElem LinearMap.IsIdempotentElem.isSymmetric_iff_orthogonal_range isSymmetric
isIdempotentElem 📖	mathematical	LinearMap.IsSymmetricProjection	IsIdempotentElem LinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule InnerProductSpace.toNormedSpace Module.End.instMul	—	—
isSymmetric 📖	mathematical	LinearMap.IsSymmetricProjection	LinearMap.IsSymmetric	—	—
sub_of_range_le_range 📖	mathematical	LinearMap.IsSymmetricProjection NormedAddCommGroup.toSeminormedAddCommGroup Submodule DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule InnerProductSpace.toNormedSpace Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder LinearMap.range RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids	LinearMap LinearMap.instSub SeminormedAddCommGroup.toAddCommGroup	—	RingHomSurjective.ids IsIdempotentElem.sub isIdempotentElem LinearMap.ext ext_inner_left isSymmetric RingHomCompTriple.ids LinearMap.IsIdempotentElem.comp_eq_right_iff LinearMap.IsSymmetric.sub

Submodule.IsCompl

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
projection_isSymmetricProjection_iff 📖	mathematical	IsCompl 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 Submodule.instPartialOrder CompleteLattice.toBoundedOrder Submodule.completeLattice	LinearMap.IsSymmetricProjection projection NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing SeminormedAddCommGroup.toAddCommGroup Submodule.IsOrtho	—	projection_isIdempotentElem projection_isSymmetric_iff
projection_isSymmetricProjection_of_isOrtho 📖	mathematical	IsCompl 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 Submodule.instPartialOrder CompleteLattice.toBoundedOrder Submodule.completeLattice Submodule.IsOrtho	LinearMap.IsSymmetricProjection projection NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing SeminormedAddCommGroup.toAddCommGroup	—	projection_isSymmetricProjection_iff
projection_isSymmetric_iff 📖	mathematical	IsCompl 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 Submodule.instPartialOrder CompleteLattice.toBoundedOrder Submodule.completeLattice	LinearMap.IsSymmetric projection NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing SeminormedAddCommGroup.toAddCommGroup Submodule.IsOrtho	—	projection.eq_1 Submodule.linearProjOfIsCompl_apply_left Submodule.subtype_apply RingHomCompTriple.ids LinearMap.comp_apply Submodule.linearProjOfIsCompl_apply_right map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass inner_zero_left IsCompl.symm projection_add_projection_eq_self inner_add_right Submodule.isOrtho_iff_inner_eq add_zero inner_add_left AddLeftCancelSemigroup.toIsLeftCancelAdd

---

← Back to Index