Basic

📁 Source: Mathlib/LinearAlgebra/SesquilinearForm/Basic.lean

Statistics

Metric	Count
Definitions IsAdjointPair, IsAlt, IsNonneg, IsOrtho, IsOrthogonal, IsOrthoᵢ, IsPairSelfAdjoint, IsPosSemidef, IsRefl, IsSelfAdjoint, IsSkewAdjoint, IsSymm, SeparatingLeft, SeparatingRight, isPairSelfAdjointSubmodule, selfAdjointSubmodule, skewAdjointSubmodule, orthogonalBilin	18
Theorems isAdjointPair_symm_iff, apply_apply_same_eq_zero_iff, apply_mul_apply_le_of_forall_zero_le, apply_mul_apply_lt_iff_linearIndependent, apply_smul_sub_smul_sub_eq, apply_sq_le_of_symm, apply_sq_lt_iff_linearIndependent_of_symm, nondegenerate_iff, nondegenerate_iff', nondegenerate_restrict_iff_disjoint_ker, not_linearIndependent_of_apply_mul_apply_eq, isSymm_iff_eq_flip, add, comp, mul, smul, sub, eq_of_add_add_eq_zero, isRefl, neg, ortho_comm, self_eq_zero, add, nonneg, smul, nondegenerate_of_not_isOrtho_basis_self, not_isOrtho_basis_self_of_separatingLeft, not_isOrtho_basis_self_of_separatingRight, separatingLeft_of_not_isOrtho_basis_self, separatingRight_iff_not_isOrtho_basis_self, add, isNonneg, isSymm, domRestrict, eq_iff, eq_zero, flip_isRefl_iff, ker_eq_bot_iff_ker_flip_eq_bot, ker_flip, ker_flip_eq_bot, nondegenerate_iff_separatingLeft, nondegenerate_iff_separatingRight, ortho_comm, add, domRestrict, eq, isRefl, nondegenerate_restrict_of_isCompl_ker, ortho_comm, ne_zero, disjoint_ker_of_nondegenerate_restrict, flip_nondegenerate, flip_separatingLeft, flip_separatingRight, isAdjointPair_id, isAdjointPair_iff_comp_eq_compl₂, isAdjointPair_one, isAdjointPair_zero, isAlt_iff_eq_neg_flip, isCompl_span_singleton_orthogonal, isNonneg_def, isNonneg_zero, isOrtho_def, isOrtho_flip, isOrtho_zero_left, isOrtho_zero_right, isOrthogonal_of_forall_apply_same, isOrthoᵢ_def, isOrthoᵢ_flip, isPairSelfAdjoint_equiv, isPosSemidef_def, isPosSemidef_zero, isSkewAdjoint_iff_neg_self_adjoint, isSymm_def, isSymm_iff_eq_flip, isSymm_zero, linearIndependent_of_isOrthoᵢ, mem_isPairSelfAdjointSubmodule, mem_selfAdjointSubmodule, mem_skewAdjointSubmodule, nondegenerate_congr_iff, nondegenerate_restrict_of_disjoint_orthogonal, not_separatingLeft_zero, ortho_smul_left, ortho_smul_right, orthogonal_span_singleton_eq_to_lin_ker, separatingLeft_congr_iff, separatingLeft_iff_ker_eq_bot, separatingLeft_iff_linear_nontrivial, separatingRight_congr_iff, separatingRight_iff_flip_ker_eq_bot, separatingRight_iff_linear_flip_nontrivial, span_singleton_inf_orthogonal_eq_bot, span_singleton_sup_orthogonal_eq_top, le_orthogonalBilin_orthogonalBilin, mem_orthogonalBilin_iff, orthogonalBilin_le	97
Total	115

LinearEquiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isAdjointPair_symm_iff 📖	mathematical	—	LinearMap.IsAdjointPair CommRing.toCommSemiring AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Semiring.toModule RingHom.id DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike Equiv.symm LinearMap.IsOrthogonal	—	Equiv.symm_apply_apply Equiv.apply_symm_apply

LinearMap

Definitions

Name	Category	Theorems
IsAdjointPair 📖	MathDef	12 math math: isAdjointPair_iff_comp_eq_compl₂, isAdjointPair_toLinearMap₂, LinearEquiv.isAdjointPair_symm_iff, isAdjointPair_one, BilinForm.isAdjointPair_iff_eq_of_nondegenerate, isAdjointPair_toLinearMap₂', isAdjointPair_id, isSkewAdjoint_iff_neg_self_adjoint, ContinuousLinearMap.isAdjointPair_inner, BilinForm.isAdjointPairLeftAdjointOfNondegenerate, isAdjointPair_inner, isAdjointPair_zero
IsAlt 📖	MathDef	3 math math: Polynomial.isAlt_wronskianBilin, BilinMap.toQuadraticMap_eq_zero, isAlt_iff_eq_neg_flip
IsNonneg 📖	CompData	5 math math: isPosSemidef_def, BilinForm.isNonneg_iff, IsPosSemidef.isNonneg, isNonneg_def, isNonneg_zero
IsOrtho 📖	MathDef	16 math math: ortho_smul_right, ortho_smul_left, IsSymm.ortho_comm, BilinForm.exists_bilinForm_self_ne_zero, IsOrthoᵢ.not_isOrtho_basis_self_of_separatingRight, BilinForm.toQuadraticMap_isOrtho, IsRefl.ortho_comm, QuadraticMap.isOrtho_polarBilin, IsAlt.ortho_comm, isOrtho_flip, isOrtho_zero_left, IsOrthoᵢ.not_isOrtho_basis_self_of_separatingLeft, Submodule.mem_orthogonalBilin_iff, QuadraticMap.associated_isOrtho, isOrtho_zero_right, isOrtho_def
IsOrthogonal 📖	MathDef	5 math math: RootPairing.RootPositiveForm.isOrthogonal_reflection, LinearEquiv.isAdjointPair_symm_iff, RootPairing.InvariantForm.isOrthogonal_reflection, IsReflective.isOrthogonal_reflection, isOrthogonal_of_forall_apply_same
IsOrthoᵢ 📖	MathDef	3 math math: BilinForm.exists_orthogonal_basis, isOrthoᵢ_def, isOrthoᵢ_flip
IsPairSelfAdjoint 📖	MathDef	2 math math: mem_isPairSelfAdjointSubmodule, isPairSelfAdjoint_equiv
IsPosSemidef 📖	CompData	4 math math: BilinForm.isPosSemidef_iff, isPosSemidef_def, isPosSemidef_iff_posSemidef_toMatrix, isPosSemidef_zero
IsRefl 📖	MathDef	3 math math: IsRefl.flip_isRefl_iff, IsSymm.isRefl, IsAlt.isRefl
IsSelfAdjoint 📖	MathDef	2 math math: mem_selfAdjointSubmodule, isSymmetric_iff_sesqForm
IsSkewAdjoint 📖	MathDef	2 math math: mem_skewAdjointSubmodule, isSkewAdjoint_iff_neg_self_adjoint
IsSymm 📖	CompData	16 math math: isSymm_zero, QuadraticMap.canLift, isPosSemidef_def, isSymm_iff_eq_flip, isSymm_dualProd, LieModule.traceForm_isSymm, RootPairing.InvariantForm.symm, isSymm_def, BilinForm.isSymm_iff, RootPairing.RootPositiveForm.symm, RootPairing.RootPositiveForm.isSymm_posForm, QuadraticForm.associated_isSymm, IsPosSemidef.isSymm, isSymm_iff_basis, RootPairing.rootForm_symmetric, isSymm_iff_isHermitian_toMatrix
SeparatingLeft 📖	MathDef	29 math math: Matrix.SeparatingLeft.toBilin', Matrix.SeparatingLeft.toLinearMap₂', BilinForm.separatingLeft_toMatrix'_iff, separatingLeft_toMatrix₂'_iff, Matrix.SeparatingLeft.toBilin, separatingLeft_iff_det_ne_zero, StrongDual.dualPairing_separatingLeft, BilinForm.separatingLeft_of_anisotropic, flip_separatingRight, separatingLeft_congr_iff, Matrix.separatingLeft_toLinearMap₂'_iff, separatingLeft_toLinearMap₂'_of_det_ne_zero', Matrix.separatingLeft_toBilin'_iff, Matrix.separatingLeft_toLinearMap₂_iff, IsOrthoᵢ.separatingLeft_of_not_isOrtho_basis_self, not_separatingLeft_zero, separatingLeft_iff_linear_nontrivial, separatingLeft_toMatrix₂_iff, QuadraticMap.separatingLeft_of_anisotropic, flip_separatingLeft, Matrix.separatingLeft_toBilin_iff, separatingLeft_iff_ker_eq_bot, separatingLeft_toLinearMap₂'_iff_det_ne_zero, IsRefl.nondegenerate_iff_separatingLeft, Matrix.separatingLeft_toLinearMap₂'_iff_separatingLeft_toLinearMap₂, BilinForm.separatingLeft_toMatrix_iff, Matrix.SeparatingLeft.toLinearMap₂, separatingLeft_of_det_ne_zero, separatingLeft_dualProd
SeparatingRight 📖	MathDef	24 math math: Matrix.SeparatingRight.toLinearMap₂, Matrix.separatingRight_toLinearMap₂'_iff, Matrix.separatingRight_toLinearMap₂_iff, Matrix.separatingRight_toBilin_iff, separatingRight_iff_det_ne_zero, separatingRight_congr_iff, separatingRight_toMatrix₂'_iff, Matrix.SeparatingRight.toLinearMap₂', BilinForm.separatingRight_toMatrix'_iff, separatingRight_iff_flip_ker_eq_bot, BilinForm.separatingRight_toMatrix_iff, flip_separatingRight, separatingRight_toLinearMap₂'_of_det_ne_zero', IsOrthoᵢ.separatingRight_iff_not_isOrtho_basis_self, Matrix.separatingRight_toBilin'_iff, separatingRight_iff_linear_flip_nontrivial, separatingRight_of_det_ne_zero, separatingRight_toMatrix₂_iff, flip_separatingLeft, Matrix.SeparatingRight.toBilin', IsRefl.nondegenerate_iff_separatingRight, separatingRight_toLinearMap₂'_iff_det_ne_zero, Matrix.SeparatingRight.toBilin, Matrix.separatingRight_toLinearMap₂'_iff_separatingRight_toLinearMap₂
isPairSelfAdjointSubmodule 📖	CompOp	1 math math: mem_isPairSelfAdjointSubmodule
selfAdjointSubmodule 📖	CompOp	1 math math: mem_selfAdjointSubmodule
skewAdjointSubmodule 📖	CompOp	1 math math: mem_skewAdjointSubmodule

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
disjoint_ker_of_nondegenerate_restrict 📖	mathematical	Nondegenerate Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike Submodule.addCommMonoid Submodule.module RingHom.id Semiring.toNonAssocSemiring domRestrict₁₂ smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing	Disjoint Submodule.instPartialOrder Submodule.instOrderBot ker LinearMap addCommMonoid module	—	smulCommClass_self Submodule.disjoint_def mem_ker
flip_nondegenerate 📖	mathematical	—	Nondegenerate flip CommSemiring.toSemiring smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction	—	smulCommClass_self flip_separatingRight flip_separatingLeft
flip_separatingLeft 📖	mathematical	—	SeparatingLeft flip CommSemiring.toSemiring smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction SeparatingRight	—	smulCommClass_self flip_separatingRight SMulCommClass.symm flip_flip
flip_separatingRight 📖	mathematical	—	SeparatingRight flip CommSemiring.toSemiring smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction SeparatingLeft	—	smulCommClass_self
isAdjointPair_id 📖	mathematical	—	IsAdjointPair	—	smulCommClass_self
isAdjointPair_iff_comp_eq_compl₂ 📖	mathematical	—	IsAdjointPair DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring instFunLike comp addCommMonoid module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction RingHomCompTriple.ids compl₂	—	smulCommClass_self RingHomCompTriple.ids ext comp_apply compl₂_apply
isAdjointPair_one 📖	mathematical	—	IsAdjointPair DFunLike.coe Module.End CommSemiring.toSemiring instFunLike RingHom.id Semiring.toNonAssocSemiring Module.End.instOne	—	smulCommClass_self isAdjointPair_id
isAdjointPair_zero 📖	mathematical	—	IsAdjointPair Pi.instZero AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	smulCommClass_self map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass semilinearMapClass
isAlt_iff_eq_neg_flip 📖	mathematical	—	IsAlt CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule CommSemiring.toSemiring LinearMap addCommMonoid module SMulCommClass.symm SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Algebra.to_smulCommClass Algebra.id instNeg addCommGroup Ring.toAddCommGroup CommRing.toRing flip	—	Algebra.to_smulCommClass SMulCommClass.symm ext smulCommClass_self IsAlt.neg congr_fun₂ add_self_eq_zero
isCompl_span_singleton_orthogonal 📖	mathematical	IsOrtho Semifield.toCommSemiring Field.toSemifield AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing Semiring.toModule DivisionSemiring.toSemiring Semifield.toDivisionSemiring RingHom.id Semiring.toNonAssocSemiring	IsCompl Submodule Submodule.instPartialOrder CompleteLattice.toBoundedOrder Submodule.completeLattice Submodule.span Set Set.instSingletonSet Submodule.orthogonalBilin Ring.toAddCommGroup DivisionRing.toRing Field.toDivisionRing	—	Algebra.to_smulCommClass disjoint_iff span_singleton_inf_orthogonal_eq_bot codisjoint_iff span_singleton_sup_orthogonal_eq_top
isNonneg_def 📖	mathematical	—	IsNonneg MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring DFunLike.coe LinearMap NonUnitalNonAssocSemiring.toAddCommMonoid Semiring.toModule instFunLike addCommMonoid module Algebra.to_smulCommClass Algebra.id	—	Algebra.to_smulCommClass
isNonneg_zero 📖	mathematical	—	IsNonneg Preorder.toLE LinearMap CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule addCommMonoid module Algebra.to_smulCommClass Algebra.id instZero	—	Algebra.to_smulCommClass le_rfl
isOrtho_def 📖	mathematical	—	IsOrtho DFunLike.coe LinearMap CommSemiring.toSemiring instFunLike addCommMonoid module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass	—	smulCommClass_self
isOrtho_flip 📖	mathematical	—	IsOrtho flip CommSemiring.toSemiring smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction	—	smulCommClass_self
isOrtho_zero_left 📖	mathematical	—	IsOrtho AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	smulCommClass_self map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass semilinearMapClass zero_apply
isOrtho_zero_right 📖	mathematical	—	IsOrtho AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	smulCommClass_self map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass semilinearMapClass
isOrthogonal_of_forall_apply_same 📖	mathematical	IsLeftRegular Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Nat.instAtLeastTwoHAddOfNat IsSymm CommRing.toCommSemiring AddCommGroup.toAddCommMonoid RingHom.id Semiring.toNonAssocSemiring CommSemiring.toSemiring DFunLike.coe LinearMap NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule instFunLike BilinForm addCommMonoid module	IsOrthogonal	—	Nat.instAtLeastTwoHAddOfNat AddRightCancelSemigroup.toIsRightCancelAdd add_assoc AddLeftCancelSemigroup.toIsLeftCancelAdd IsSymm.eq map_add SemilinearMapClass.toAddHomClass semilinearMapClass
isOrthoᵢ_def 📖	mathematical	—	IsOrthoᵢ DFunLike.coe LinearMap CommSemiring.toSemiring instFunLike addCommMonoid module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass	—	smulCommClass_self
isOrthoᵢ_flip 📖	mathematical	—	IsOrthoᵢ flip CommSemiring.toSemiring smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction	—	smulCommClass_self
isPairSelfAdjoint_equiv 📖	mathematical	—	IsPairSelfAdjoint CommRing.toCommSemiring AddCommGroup.toAddCommMonoid RingHom.id Semiring.toNonAssocSemiring CommSemiring.toSemiring DFunLike.coe Module.End instFunLike compl₁₂ smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing LinearEquiv.toLinearMap RingHomInvPair.ids LinearEquiv addCommMonoid module CommSemiring.toCommMonoid EquivLike.toFunLike LinearEquiv.instEquivLike LinearEquiv.conj LinearEquiv.symm	—	smulCommClass_self RingHomInvPair.ids RingHomCompTriple.ids ext LinearEquiv.apply_symm_apply LinearEquiv.surjective
isPosSemidef_def 📖	mathematical	—	IsPosSemidef IsSymm IsNonneg RingHom.id Semiring.toNonAssocSemiring CommSemiring.toSemiring	—	Algebra.to_smulCommClass IsPosSemidef.isSymm IsPosSemidef.isNonneg
isPosSemidef_zero 📖	mathematical	—	IsPosSemidef Preorder.toLE LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule addCommMonoid module Algebra.to_smulCommClass Algebra.id instZero	—	Algebra.to_smulCommClass isSymm_zero isNonneg_zero
isSkewAdjoint_iff_neg_self_adjoint 📖	mathematical	—	IsSkewAdjoint IsAdjointPair CommRing.toCommSemiring AddCommGroup.toAddCommMonoid RingHom.id Semiring.toNonAssocSemiring CommSemiring.toSemiring LinearMap addCommMonoid module smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing instNeg addCommGroup	—	smulCommClass_self map_neg DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass semilinearMapClass
isSymm_def 📖	mathematical	—	IsSymm DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike LinearMap RingHom.id NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule instFunLike addCommMonoid module Algebra.to_smulCommClass Algebra.id	—	Algebra.to_smulCommClass
isSymm_iff_eq_flip 📖	mathematical	—	IsSymm RingHom.id Semiring.toNonAssocSemiring CommSemiring.toSemiring flip NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule	—	Algebra.to_smulCommClass isSymm_def BilinMap.isSymm_iff_eq_flip
isSymm_zero 📖	mathematical	—	IsSymm LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule addCommMonoid module Algebra.to_smulCommClass Algebra.id instZero	—	Algebra.to_smulCommClass map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass
linearIndependent_of_isOrthoᵢ 📖	mathematical	IsOrthoᵢ Semifield.toCommSemiring Field.toSemifield AddCommGroup.toAddCommMonoid IsOrtho	LinearIndependent DivisionSemiring.toSemiring Semifield.toDivisionSemiring	—	smulCommClass_self linearIndependent_iff' map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass semilinearMapClass zero_apply Finset.sum_eq_single_of_mem isOrthoᵢ_def smul_zero map_eq_zero DivisionRing.toNontrivial RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass smul_eq_zero DivisionSemiring.to_moduleIsTorsionFree IsDomain.toIsCancelMulZero Field.isDomain Finset.sum_congr map_smulₛₗ₂ map_sum₂
mem_isPairSelfAdjointSubmodule 📖	mathematical	—	Module.End CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Submodule addCommMonoid RingHom.id Semiring.toNonAssocSemiring module smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing SetLike.instMembership Submodule.setLike isPairSelfAdjointSubmodule IsPairSelfAdjoint DFunLike.coe instFunLike	—	smulCommClass_self
mem_selfAdjointSubmodule 📖	mathematical	—	Module.End CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Submodule addCommMonoid RingHom.id Semiring.toNonAssocSemiring module smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing SetLike.instMembership Submodule.setLike selfAdjointSubmodule IsSelfAdjoint DFunLike.coe instFunLike	—	smulCommClass_self
mem_skewAdjointSubmodule 📖	mathematical	—	Module.End CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Submodule addCommMonoid RingHom.id Semiring.toNonAssocSemiring module smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing SetLike.instMembership Submodule.setLike skewAdjointSubmodule IsSkewAdjoint DFunLike.coe instFunLike	—	smulCommClass_self isSkewAdjoint_iff_neg_self_adjoint
nondegenerate_congr_iff 📖	mathematical	—	Nondegenerate RingHom.id Semiring.toNonAssocSemiring CommSemiring.toSemiring DFunLike.coe LinearEquiv RingHomInvPair.ids LinearMap addCommMonoid module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction EquivLike.toFunLike LinearEquiv.instEquivLike LinearEquiv.arrowCongr RingHomCompTriple.ids LinearEquiv.refl	—	smulCommClass_self RingHomInvPair.ids RingHomCompTriple.ids separatingLeft_congr_iff separatingRight_congr_iff Nondegenerate.congr
nondegenerate_restrict_of_disjoint_orthogonal 📖	mathematical	IsRefl CommRing.toCommSemiring AddCommGroup.toAddCommMonoid RingHom.id Semiring.toNonAssocSemiring CommSemiring.toSemiring Disjoint Submodule Submodule.instPartialOrder Submodule.instOrderBot Submodule.orthogonalBilin	Nondegenerate SetLike.instMembership Submodule.setLike Submodule.addCommMonoid Submodule.module domRestrict₁₂ smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing	—	smulCommClass_self IsRefl.nondegenerate_iff_separatingLeft IsRefl.domRestrict Submodule.mk_eq_zero Submodule.mem_bot Disjoint.le_bot IsRefl.ortho_comm
not_separatingLeft_zero 📖	mathematical	—	SeparatingLeft LinearMap CommSemiring.toSemiring addCommMonoid module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction instZero	—	smulCommClass_self exists_ne
ortho_smul_left 📖	mathematical	—	IsOrtho Semifield.toCommSemiring Field.toSemifield AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Module.toDistribMulAction	—	smulCommClass_self map_smulₛₗ₂ smul_zero smul_eq_zero DivisionSemiring.to_moduleIsTorsionFree IsDomain.toIsCancelMulZero Field.isDomain map_eq_zero DivisionRing.toNontrivial RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass
ortho_smul_right 📖	mathematical	—	IsOrtho Semifield.toCommSemiring Field.toSemifield AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Module.toDistribMulAction	—	smulCommClass_self MulActionSemiHomClass.map_smulₛₗ SemilinearMapClass.toMulActionSemiHomClass semilinearMapClass smul_zero smul_eq_zero DivisionSemiring.to_moduleIsTorsionFree IsDomain.toIsCancelMulZero Field.isDomain DivisionRing.toNontrivial RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass
orthogonal_span_singleton_eq_to_lin_ker 📖	mathematical	—	Submodule.orthogonalBilin Field.toCommRing RingHom.id Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Submodule.span AddCommGroup.toAddCommMonoid Set Set.instSingletonSet ker DFunLike.coe LinearMap addCommMonoid module smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing instFunLike	—	smulCommClass_self Submodule.ext one_smul isOrtho_def map_smulₛₗ₂ smul_eq_zero DivisionSemiring.to_moduleIsTorsionFree IsDomain.toIsCancelMulZero Field.isDomain
separatingLeft_congr_iff 📖	mathematical	—	SeparatingLeft RingHom.id Semiring.toNonAssocSemiring CommSemiring.toSemiring DFunLike.coe LinearEquiv RingHomInvPair.ids LinearMap addCommMonoid module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction EquivLike.toFunLike LinearEquiv.instEquivLike LinearEquiv.arrowCongr RingHomCompTriple.ids LinearEquiv.refl	—	smulCommClass_self RingHomInvPair.ids RingHomCompTriple.ids ext LinearEquiv.symm_apply_apply SeparatingLeft.congr
separatingLeft_iff_ker_eq_bot 📖	mathematical	—	SeparatingLeft ker LinearMap CommSemiring.toSemiring addCommMonoid module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Bot.bot Submodule Submodule.instBot	—	smulCommClass_self separatingLeft_iff_linear_nontrivial ker_eq_bot'
separatingLeft_iff_linear_nontrivial 📖	mathematical	—	SeparatingLeft AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	smulCommClass_self Zero.instNonempty ext zero_apply
separatingRight_congr_iff 📖	mathematical	—	SeparatingRight RingHom.id Semiring.toNonAssocSemiring CommSemiring.toSemiring DFunLike.coe LinearEquiv RingHomInvPair.ids LinearMap addCommMonoid module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction EquivLike.toFunLike LinearEquiv.instEquivLike LinearEquiv.arrowCongr RingHomCompTriple.ids LinearEquiv.refl	—	smulCommClass_self RingHomInvPair.ids separatingLeft_congr_iff
separatingRight_iff_flip_ker_eq_bot 📖	mathematical	—	SeparatingRight ker LinearMap CommSemiring.toSemiring addCommMonoid module SMulCommClass.symm SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid flip Bot.bot Submodule Submodule.instBot	—	smulCommClass_self SMulCommClass.symm flip_separatingLeft separatingLeft_iff_ker_eq_bot
separatingRight_iff_linear_flip_nontrivial 📖	mathematical	—	SeparatingRight AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	smulCommClass_self SMulCommClass.symm flip_separatingLeft separatingLeft_iff_linear_nontrivial
span_singleton_inf_orthogonal_eq_bot 📖	mathematical	IsOrtho Semifield.toCommSemiring Field.toSemifield AddCommGroup.toAddCommMonoid	Submodule DivisionSemiring.toSemiring Semifield.toDivisionSemiring Submodule.instMin Submodule.span Set Set.instSingletonSet Submodule.orthogonalBilin Field.toCommRing Bot.bot Submodule.instBot	—	smulCommClass_self Finset.coe_singleton eq_bot_iff Submodule.mem_span_finset Finset.sum_singleton smul_eq_zero DivisionSemiring.to_moduleIsTorsionFree IsDomain.toIsCancelMulZero Field.isDomain MulActionSemiHomClass.map_smulₛₗ SemilinearMapClass.toMulActionSemiHomClass semilinearMapClass isOrtho_def DivisionRing.toNontrivial RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass zero_smul Submodule.mem_bot
span_singleton_sup_orthogonal_eq_top 📖	mathematical	IsOrtho Semifield.toCommSemiring Field.toSemifield AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing Semiring.toModule DivisionSemiring.toSemiring Semifield.toDivisionSemiring RingHom.id Semiring.toNonAssocSemiring	Submodule SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Submodule.completeLattice Submodule.span Set Set.instSingletonSet Submodule.orthogonalBilin Ring.toAddCommGroup DivisionRing.toRing Field.toDivisionRing Top.top Submodule.instTop	—	Algebra.to_smulCommClass smulCommClass_self orthogonal_span_singleton_eq_to_lin_ker span_singleton_sup_ker_eq_top

LinearMap.BilinForm

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
apply_apply_same_eq_zero_iff 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.instFunLike LinearMap.BilinForm LinearMap.addCommMonoid LinearMap.module LinearMap.IsSymm	Submodule SetLike.instMembership Submodule.setLike LinearMap.ker	—	LinearMap.mem_ker LinearMap.ext apply_sq_le_of_symm eq_zero_of_pow_eq_zero isReduced_of_noZeroDivisors IsStrictOrderedRing.noZeroDivisors AddGroup.existsAddOfLE le_antisymm MulZeroClass.zero_mul sq_nonneg IsOrderedRing.toPosMulMono IsStrictOrderedRing.toIsOrderedRing IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid
apply_mul_apply_le_of_forall_zero_le 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.instFunLike LinearMap.BilinForm LinearMap.addCommMonoid LinearMap.module	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	apply_smul_sub_smul_sub_eq lt_or_ge sub_nonneg covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing nonneg_of_mul_nonneg_right IsStrictOrderedRing.toPosMulStrictMono le_antisymm mul_comm eq_neg_iff_add_eq_zero map_sub DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass zero_sub sub_zero map_add SemilinearMapClass.toAddHomClass zero_add add_zero neg_mul MulZeroClass.mul_zero mul_self_nonneg AddGroup.existsAddOfLE IsOrderedRing.toPosMulMono
apply_mul_apply_lt_iff_linearIndependent 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.instFunLike LinearMap.BilinForm LinearMap.addCommMonoid LinearMap.module	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib LinearIndependent Matrix.vecCons Matrix.vecEmpty	—	eq_or_ne map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass Mathlib.Tactic.Contrapose.contrapose₁ Mathlib.Tactic.Push.not_forall_eq Mathlib.Tactic.Push.not_and_eq LinearIndependent.pair_iff zero_smul zero_add IsDomain.toIsCancelMulZero MulZeroClass.mul_zero add_zero MulZeroClass.zero_mul Algebra.to_smulCommClass map_smul SemilinearMapClass.toMulActionSemiHomClass neg_smul add_eq_zero_iff_eq_neg' map_neg mul_neg neg_neg neg_mul IsStrictOrderedRing.noZeroDivisors AddGroup.existsAddOfLE le_of_eq mul_right_injective₀ IsCancelMulZero.toIsLeftCancelMulZero 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 not_linearIndependent_of_apply_mul_apply_eq le_antisymm apply_mul_apply_le_of_forall_zero_le
apply_smul_sub_smul_sub_eq 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.instFunLike LinearMap.BilinForm LinearMap.addCommMonoid LinearMap.module SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing	—	Algebra.to_smulCommClass map_sub DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass map_smul SemilinearMapClass.toMulActionSemiHomClass mul_comm mul_sub mul_left_comm Mathlib.Tactic.Abel.unfold_sub Mathlib.Tactic.Abel.subst_into_addg 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.Meta.NormNum.IsNat.to_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_neg Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Abel.term_add_termg Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Abel.zero_termg Mathlib.Tactic.Abel.const_add_termg add_zero
apply_sq_le_of_symm 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.instFunLike LinearMap.BilinForm LinearMap.addCommMonoid LinearMap.module LinearMap.IsSymm	Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	sq Algebra.to_smulCommClass LinearMap.IsSymm.eq RingHom.id_apply apply_mul_apply_le_of_forall_zero_le
apply_sq_lt_iff_linearIndependent_of_symm 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.instFunLike LinearMap.BilinForm LinearMap.addCommMonoid LinearMap.module LinearMap.IsSymm	Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Distrib.toMul NonUnitalNonAssocSemiring.toDistrib LinearIndependent Matrix.vecCons Matrix.vecEmpty	—	sq Algebra.to_smulCommClass LinearMap.IsSymm.eq RingHom.id_apply apply_mul_apply_lt_iff_linearIndependent
nondegenerate_iff 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.instFunLike LinearMap.BilinForm LinearMap.addCommMonoid LinearMap.module LinearMap.IsSymm	LinearMap.Nondegenerate NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	LinearMap.IsRefl.nondegenerate_iff_separatingLeft LinearMap.IsSymm.isRefl smulCommClass_self apply_apply_same_eq_zero_iff map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass
nondegenerate_iff' 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.instFunLike LinearMap.BilinForm LinearMap.addCommMonoid LinearMap.module LinearMap.IsSymm	LinearMap.Nondegenerate Preorder.toLT	—	nondegenerate_iff Mathlib.Tactic.Contrapose.contrapose_iff₁ Mathlib.Tactic.Push.not_forall_eq map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass le_antisymm
nondegenerate_restrict_iff_disjoint_ker 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.instFunLike LinearMap.BilinForm LinearMap.addCommMonoid LinearMap.module LinearMap.IsSymm	LinearMap.Nondegenerate Submodule SetLike.instMembership Submodule.setLike Submodule.addCommMonoid Submodule.module LinearMap.domRestrict₁₂ Disjoint Submodule.instPartialOrder Submodule.instOrderBot LinearMap.ker	—	LinearMap.disjoint_ker_of_nondegenerate_restrict LinearMap.IsSymm.isRefl LinearMap.IsRefl.nondegenerate_iff_separatingLeft apply_apply_same_eq_zero_iff Disjoint.eq_bot
not_linearIndependent_of_apply_mul_apply_eq 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.instFunLike LinearMap.BilinForm LinearMap.addCommMonoid LinearMap.module Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	LinearIndependent Matrix.vecCons Matrix.vecEmpty	—	ne_of_lt mul_eq_zero_of_right sub_eq_zero_of_eq apply_smul_sub_smul_sub_eq LinearIndependent.ne_zero instNontrivialOfCharZero IsStrictOrderedRing.toCharZero sub_eq_zero LinearIndependent.eq_zero_of_pair add_comm neg_smul sub_eq_add_neg

LinearMap.BilinMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isSymm_iff_eq_flip 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike LinearMap.BilinMap LinearMap.addCommMonoid LinearMap.module LinearMap.flip	—	—

LinearMap.IsAdjointPair

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add 📖	mathematical	LinearMap.IsAdjointPair	Pi.instAdd AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup	—	smulCommClass_self Pi.add_apply LinearMap.map_add₂ LinearMap.map_add
comp 📖	—	LinearMap.IsAdjointPair	—	—	smulCommClass_self
mul 📖	mathematical	LinearMap.IsAdjointPair DFunLike.coe Module.End CommSemiring.toSemiring LinearMap.instFunLike RingHom.id Semiring.toNonAssocSemiring	Module.End.instMul	—	smulCommClass_self comp
smul 📖	mathematical	LinearMap.IsAdjointPair CommRing.toCommSemiring AddCommGroup.toAddCommMonoid RingHom.id Semiring.toNonAssocSemiring CommSemiring.toSemiring	Function.hasSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	smulCommClass_self map_smul SemilinearMapClass.toMulActionSemiHomClass LinearMap.semilinearMapClass
sub 📖	mathematical	LinearMap.IsAdjointPair CommRing.toCommSemiring AddCommGroup.toAddCommMonoid RingHom.id Semiring.toNonAssocSemiring CommSemiring.toSemiring	Pi.instSub SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup	—	smulCommClass_self Pi.sub_apply LinearMap.map_sub₂ LinearMap.map_sub

LinearMap.IsAlt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eq_of_add_add_eq_zero 📖	mathematical	LinearMap.IsAlt AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	DFunLike.coe LinearMap CommSemiring.toSemiring LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid Module.toDistribMulAction	—	smulCommClass_self SemilinearMapClass.toAddHomClass LinearMap.semilinearMapClass map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass add_left_cancel IsCancelAdd.toIsLeftCancelAdd add_comm add_zero zero_add
isRefl 📖	mathematical	LinearMap.IsAlt AddCommGroup.toAddCommMonoid	LinearMap.IsRefl	—	smulCommClass_self neg neg_zero
neg 📖	mathematical	LinearMap.IsAlt AddCommGroup.toAddCommMonoid	NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid DFunLike.coe LinearMap CommSemiring.toSemiring LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction	—	smulCommClass_self self_eq_zero map_add SemilinearMapClass.toAddHomClass LinearMap.semilinearMapClass zero_add add_zero
ortho_comm 📖	mathematical	LinearMap.IsAlt AddCommGroup.toAddCommMonoid	LinearMap.IsOrtho	—	smulCommClass_self LinearMap.IsRefl.ortho_comm isRefl
self_eq_zero 📖	mathematical	LinearMap.IsAlt	DFunLike.coe LinearMap CommSemiring.toSemiring LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass	—	smulCommClass_self

LinearMap.IsNonneg

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add 📖	mathematical	LinearMap.IsNonneg Preorder.toLE	LinearMap CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule LinearMap.addCommMonoid LinearMap.module Algebra.to_smulCommClass Algebra.id LinearMap.instAdd	—	Algebra.to_smulCommClass add_nonneg nonneg
nonneg 📖	mathematical	LinearMap.IsNonneg	MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring DFunLike.coe LinearMap NonUnitalNonAssocSemiring.toAddCommMonoid Semiring.toModule LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module Algebra.to_smulCommClass Algebra.id	—	Algebra.to_smulCommClass
smul 📖	mathematical	LinearMap.IsNonneg Preorder.toLE MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring	LinearMap NonUnitalNonAssocSemiring.toAddCommMonoid Semiring.toModule LinearMap.addCommMonoid LinearMap.module Algebra.to_smulCommClass Algebra.id LinearMap.instSMul DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid LinearMap.instDistribMulAction Module.toDistribMulAction LinearMap.instSMulCommClass	—	Algebra.to_smulCommClass LinearMap.instSMulCommClass mul_nonneg nonneg

LinearMap.IsOrthoᵢ

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
nondegenerate_of_not_isOrtho_basis_self 📖	mathematical	LinearMap.IsOrthoᵢ RingHom.id Semiring.toNonAssocSemiring CommSemiring.toSemiring DFunLike.coe Module.Basis Module.Basis.instFunLike LinearMap.IsOrtho	LinearMap.Nondegenerate	—	smulCommClass_self separatingLeft_of_not_isOrtho_basis_self separatingRight_iff_not_isOrtho_basis_self
not_isOrtho_basis_self_of_separatingLeft 📖	mathematical	LinearMap.IsOrthoᵢ DFunLike.coe Module.Basis CommSemiring.toSemiring Module.Basis.instFunLike LinearMap.SeparatingLeft	LinearMap.IsOrtho	—	smulCommClass_self Module.Basis.ne_zero RingHomInvPair.ids LinearEquiv.surjective Module.Basis.repr_symm_apply Finsupp.linearCombination_apply Finsupp.sum.eq_1 map_sum DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass Finset.sum_eq_zero MulActionSemiHomClass.map_smulₛₗ SemilinearMapClass.toMulActionSemiHomClass eq_or_ne smul_zero
not_isOrtho_basis_self_of_separatingRight 📖	mathematical	LinearMap.IsOrthoᵢ DFunLike.coe Module.Basis CommSemiring.toSemiring Module.Basis.instFunLike LinearMap.SeparatingRight	LinearMap.IsOrtho	—	smulCommClass_self LinearMap.isOrtho_flip not_isOrtho_basis_self_of_separatingLeft LinearMap.isOrthoᵢ_flip LinearMap.flip_separatingLeft
separatingLeft_of_not_isOrtho_basis_self 📖	mathematical	LinearMap.IsOrthoᵢ RingHom.id Semiring.toNonAssocSemiring CommSemiring.toSemiring DFunLike.coe Module.Basis Module.Basis.instFunLike LinearMap.IsOrtho	LinearMap.SeparatingLeft	—	smulCommClass_self RingHomInvPair.ids LinearEquiv.surjective LinearEquiv.map_eq_zero_iff Finsupp.ext Finsupp.zero_apply smul_eq_zero IsDomain.toIsCancelMulZero Finset.sum_eq_single RingHom.id_apply smul_zero Finsupp.notMem_support_iff zero_smul Finset.sum_congr LinearMap.map_smulₛₗ₂ LinearMap.map_sum₂ Module.Basis.repr_symm_apply
separatingRight_iff_not_isOrtho_basis_self 📖	mathematical	LinearMap.IsOrthoᵢ RingHom.id Semiring.toNonAssocSemiring CommSemiring.toSemiring DFunLike.coe Module.Basis Module.Basis.instFunLike LinearMap.IsOrtho	LinearMap.SeparatingRight	—	smulCommClass_self LinearMap.flip_separatingLeft separatingLeft_of_not_isOrtho_basis_self LinearMap.isOrthoᵢ_flip LinearMap.isOrtho_flip

LinearMap.IsPosSemidef

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add 📖	mathematical	LinearMap.IsPosSemidef Preorder.toLE	LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.addCommMonoid LinearMap.module Algebra.to_smulCommClass Algebra.id LinearMap.instAdd	—	Algebra.to_smulCommClass LinearMap.isPosSemidef_def LinearMap.IsSymm.add isSymm LinearMap.IsNonneg.add isNonneg
isNonneg 📖	mathematical	LinearMap.IsPosSemidef	LinearMap.IsNonneg RingHom.id Semiring.toNonAssocSemiring CommSemiring.toSemiring	—	Algebra.to_smulCommClass
isSymm 📖	mathematical	LinearMap.IsPosSemidef	LinearMap.IsSymm	—	Algebra.to_smulCommClass

LinearMap.IsRefl

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
domRestrict 📖	mathematical	LinearMap.IsRefl	Submodule CommSemiring.toSemiring SetLike.instMembership Submodule.setLike Submodule.addCommMonoid Submodule.module LinearMap.domRestrict₁₂ smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction	—	smulCommClass_self
eq_iff 📖	mathematical	LinearMap.IsRefl	DFunLike.coe LinearMap CommSemiring.toSemiring LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass	—	smulCommClass_self
eq_zero 📖	—	LinearMap.IsRefl DFunLike.coe LinearMap CommSemiring.toSemiring LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass	—	—	smulCommClass_self
flip_isRefl_iff 📖	mathematical	—	LinearMap.IsRefl LinearMap.flip CommSemiring.toSemiring smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction	—	smulCommClass_self
ker_eq_bot_iff_ker_flip_eq_bot 📖	mathematical	LinearMap.IsRefl	LinearMap.ker LinearMap CommSemiring.toSemiring LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Bot.bot Submodule Submodule.instBot SMulCommClass.symm SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero LinearMap.flip	—	smulCommClass_self SMulCommClass.symm ker_flip
ker_flip 📖	mathematical	LinearMap.IsRefl	LinearMap.ker LinearMap CommSemiring.toSemiring LinearMap.addCommMonoid LinearMap.module SMulCommClass.symm SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid LinearMap.flip	—	smulCommClass_self Submodule.ext SMulCommClass.symm eq_iff
ker_flip_eq_bot 📖	mathematical	LinearMap.IsRefl LinearMap.ker LinearMap CommSemiring.toSemiring LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Bot.bot Submodule Submodule.instBot	SMulCommClass.symm SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero LinearMap.flip	—	smulCommClass_self SMulCommClass.symm ker_flip
nondegenerate_iff_separatingLeft 📖	mathematical	LinearMap.IsRefl CommRing.toCommSemiring AddCommGroup.toAddCommMonoid RingHom.id Semiring.toNonAssocSemiring CommSemiring.toSemiring	LinearMap.Nondegenerate LinearMap.SeparatingLeft	—	smulCommClass_self SMulCommClass.symm LinearMap.separatingRight_iff_flip_ker_eq_bot ker_eq_bot_iff_ker_flip_eq_bot LinearMap.separatingLeft_iff_ker_eq_bot
nondegenerate_iff_separatingRight 📖	mathematical	LinearMap.IsRefl CommRing.toCommSemiring AddCommGroup.toAddCommMonoid RingHom.id Semiring.toNonAssocSemiring CommSemiring.toSemiring	LinearMap.Nondegenerate LinearMap.SeparatingRight	—	smulCommClass_self LinearMap.separatingLeft_iff_ker_eq_bot SMulCommClass.symm ker_eq_bot_iff_ker_flip_eq_bot LinearMap.separatingRight_iff_flip_ker_eq_bot
ortho_comm 📖	mathematical	LinearMap.IsRefl	LinearMap.IsOrtho	—	smulCommClass_self eq_zero

LinearMap.IsSymm

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add 📖	mathematical	LinearMap.IsSymm	LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.addCommMonoid LinearMap.module Algebra.to_smulCommClass Algebra.id LinearMap.instAdd	—	Algebra.to_smulCommClass map_add AddMonoidHomClass.toAddHomClass RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass eq
domRestrict 📖	mathematical	LinearMap.IsSymm	Submodule CommSemiring.toSemiring SetLike.instMembership Submodule.setLike Submodule.addCommMonoid Submodule.module LinearMap.domRestrict₁₂ NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Algebra.to_smulCommClass Algebra.id RingHom.id	—	Algebra.to_smulCommClass eq
eq 📖	mathematical	LinearMap.IsSymm	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike LinearMap RingHom.id NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module Algebra.to_smulCommClass Algebra.id	—	Algebra.to_smulCommClass
isRefl 📖	mathematical	LinearMap.IsSymm	LinearMap.IsRefl NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Semiring.toModule RingHom.id	—	Algebra.to_smulCommClass eq map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass
nondegenerate_restrict_of_isCompl_ker 📖	mathematical	LinearMap.IsSymm CommRing.toCommSemiring AddCommGroup.toAddCommMonoid RingHom.id Semiring.toNonAssocSemiring CommSemiring.toSemiring IsCompl Submodule Submodule.instPartialOrder CompleteLattice.toBoundedOrder Submodule.completeLattice LinearMap.ker LinearMap NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule LinearMap.addCommMonoid LinearMap.module Algebra.to_smulCommClass Algebra.id	LinearMap.Nondegenerate SetLike.instMembership Submodule.setLike Submodule.addCommMonoid Submodule.module LinearMap.domRestrict₁₂	—	Algebra.to_smulCommClass isRefl LinearMap.IsRefl.nondegenerate_iff_separatingLeft LinearMap.ext Submodule.mem_sup IsCompl.sup_eq_top Submodule.mem_top map_add SemilinearMapClass.toAddHomClass LinearMap.semilinearMapClass eq LinearMap.mem_ker add_zero IsCompl.inf_eq_bot
ortho_comm 📖	mathematical	LinearMap.IsSymm	LinearMap.IsOrtho NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Semiring.toModule RingHom.id	—	Algebra.to_smulCommClass LinearMap.IsRefl.ortho_comm isRefl

LinearMap.SeparatingLeft

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ne_zero 📖	—	LinearMap.SeparatingLeft	—	—	smulCommClass_self LinearMap.not_separatingLeft_zero

Submodule

Definitions

Name	Category	Theorems
orthogonalBilin 📖	CompOp	9 math math: orthogonalBilin_le, LinearMap.span_singleton_sup_orthogonal_eq_top, orthogonalBilin_innerₗ, bilinFormOfRealInner_orthogonal, mem_orthogonalBilin_iff, LinearMap.span_singleton_inf_orthogonal_eq_bot, le_orthogonalBilin_orthogonalBilin, LinearMap.isCompl_span_singleton_orthogonal, LinearMap.orthogonal_span_singleton_eq_to_lin_ker

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
le_orthogonalBilin_orthogonalBilin 📖	mathematical	LinearMap.IsRefl CommRing.toCommSemiring AddCommGroup.toAddCommMonoid	Submodule CommSemiring.toSemiring Preorder.toLE PartialOrder.toPreorder instPartialOrder orthogonalBilin	—	smulCommClass_self
mem_orthogonalBilin_iff 📖	mathematical	—	Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership setLike orthogonalBilin LinearMap.IsOrtho	—	smulCommClass_self
orthogonalBilin_le 📖	mathematical	Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Preorder.toLE PartialOrder.toPreorder instPartialOrder	orthogonalBilin	—	smulCommClass_self

---

← Back to Index