Orthogonal

📁 Source: Mathlib/LinearAlgebra/BilinearForm/Orthogonal.lean

Statistics

Metric	Count
Definitions IsOrtho, iIsOrtho, orthogonal	3
Theorems ortho_comm, ortho_comm, ortho_comm, eq_top_of_restrict_nondegenerate_of_orthogonal_eq_bot, finrank_add_finrank_orthogonal, finrank_orthogonal, nondegenerate_iff_not_isOrtho_basis_self, not_isOrtho_basis_self_of_nondegenerate, iIsOrtho_def, inf_orthogonal_self_le_ker_restrict, isCompl_orthogonal_iff_disjoint, isCompl_orthogonal_of_restrict_nondegenerate, isCompl_span_singleton_orthogonal, isOrtho_def, isOrtho_smul_left, isOrtho_smul_right, isOrtho_zero_left, isOrtho_zero_right, ker_restrict_eq_of_codisjoint, le_orthogonal_orthogonal, linearIndependent_of_iIsOrtho, mem_orthogonal_iff, ne_zero_of_not_isOrtho_self, nondegenerate_restrict_of_disjoint_orthogonal, orthogonal_bot, orthogonal_eq_bot_iff, orthogonal_eq_top_iff, orthogonal_le, orthogonal_orthogonal, orthogonal_span_singleton_eq_toLin_ker, orthogonal_top_eq_bot, orthogonal_top_eq_ker, restrict_nondegenerate_iff_isCompl_orthogonal, restrict_nondegenerate_orthogonal_spanSingleton, span_singleton_inf_orthogonal_eq_bot, span_singleton_sup_orthogonal_eq_top, toLin_restrict_ker_eq_inf_orthogonal, toLin_restrict_range_dualCoannihilator_eq_orthogonal	38
Total	41

LinearMap.BilinForm

Definitions

Name	Category	Theorems
IsOrtho 📖	MathDef	11 math math: isOrtho_smul_right, IsAlt.ortho_comm, IsRefl.ortho_comm, isOrtho_smul_left, isOrtho_zero_right, isOrtho_zero_left, mem_orthogonal_iff, IsSymm.ortho_comm, isOrtho_def, iIsOrtho.not_isOrtho_basis_self_of_nondegenerate, iIsOrtho.nondegenerate_iff_not_isOrtho_basis_self
iIsOrtho 📖	MathDef	1 math math: iIsOrtho_def
orthogonal 📖	CompOp	27 math math: restrict_nondegenerate_iff_isCompl_orthogonal, restrict_nondegenerate_orthogonal_spanSingleton, span_singleton_inf_orthogonal_eq_bot, isCompl_orthogonal_iff_disjoint, orthogonal_eq_bot_iff, inf_orthogonal_self_le_ker_restrict, RootPairing.orthogonal_corootSpan_eq, orthogonal_span_singleton_eq_toLin_ker, finrank_orthogonal, mem_orthogonal_iff, LieAlgebra.IsKilling.orthogonal_span_coroot_eq_ker, orthogonal_top_eq_ker, le_orthogonal_orthogonal, orthogonal_bot, LieAlgebra.InvariantForm.orthogonal_toSubmodule, orthogonal_le, orthogonal_orthogonal, orthogonal_eq_top_iff, toLin_restrict_ker_eq_inf_orthogonal, orthogonal_top_eq_bot, LieIdeal.toSubmodule_killingCompl, toLin_restrict_range_dualCoannihilator_eq_orthogonal, finrank_add_finrank_orthogonal, isCompl_orthogonal_of_restrict_nondegenerate, RootPairing.orthogonal_rootSpan_eq, isCompl_span_singleton_orthogonal, span_singleton_sup_orthogonal_eq_top

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eq_top_of_restrict_nondegenerate_of_orthogonal_eq_bot 📖	mathematical	IsRefl Semifield.toCommSemiring Field.toSemifield AddCommGroup.toAddCommMonoid Nondegenerate Submodule CommSemiring.toSemiring SetLike.instMembership Submodule.setLike Submodule.addCommMonoid Submodule.module restrict orthogonal Bot.bot Submodule.instBot	Top.top DivisionSemiring.toSemiring Semifield.toDivisionSemiring Submodule.instTop	—	IsCompl.sup_eq_top isCompl_orthogonal_of_restrict_nondegenerate sup_bot_eq
finrank_add_finrank_orthogonal 📖	mathematical	IsRefl Semifield.toCommSemiring Field.toSemifield AddCommGroup.toAddCommMonoid	Module.finrank Submodule DivisionSemiring.toSemiring Semifield.toDivisionSemiring SetLike.instMembership Submodule.setLike Submodule.addCommMonoid Submodule.module CommSemiring.toSemiring orthogonal Subspace Field.toDivisionRing DivisionRing.toDivisionSemiring Submodule.instMin Top.top Submodule.instTop	—	RingHomSurjective.ids toLin_restrict_ker_eq_inf_orthogonal toLin_restrict_range_dualCoannihilator_eq_orthogonal Submodule.finrank_map_subtype_eq Algebra.to_smulCommClass Subspace.finrank_add_finrank_dualCoannihilator_eq add_comm add_assoc LinearMap.finrank_range_add_finrank_ker FiniteDimensional.finiteDimensional_submodule
finrank_orthogonal 📖	mathematical	Nondegenerate Semifield.toCommSemiring Field.toSemifield AddCommGroup.toAddCommMonoid IsRefl	Module.finrank Submodule CommSemiring.toSemiring SetLike.instMembership Submodule.setLike orthogonal DivisionSemiring.toSemiring Semifield.toDivisionSemiring Submodule.addCommMonoid Submodule.module	—	finrank_add_finrank_orthogonal add_zero finrank_bot IsLocalRing.toNontrivial Field.instIsLocalRing inf_bot_eq orthogonal_top_eq_bot
iIsOrtho_def 📖	mathematical	—	iIsOrtho DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.instFunLike LinearMap.BilinForm LinearMap.addCommMonoid LinearMap.module MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	—
inf_orthogonal_self_le_ker_restrict 📖	mathematical	IsRefl	Submodule CommSemiring.toSemiring Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder Submodule.instMin orthogonal Submodule.map SetLike.instMembership Submodule.setLike Submodule.addCommMonoid Submodule.module RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids Submodule.subtype LinearMap.ker LinearMap NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.addCommMonoid LinearMap.module restrict	—	RingHomSurjective.ids LinearMap.ext
isCompl_orthogonal_iff_disjoint 📖	mathematical	IsRefl Semifield.toCommSemiring Field.toSemifield AddCommGroup.toAddCommMonoid	IsCompl Submodule DivisionSemiring.toSemiring Semifield.toDivisionSemiring Submodule.instPartialOrder CompleteLattice.toBoundedOrder Submodule.completeLattice orthogonal Disjoint Submodule.instOrderBot	—	IsCompl.disjoint codisjoint_iff Submodule.eq_top_of_finrank_eq LE.le.antisymm Submodule.finrank_le commRing_strongRankCondition IsLocalRing.toNontrivial Field.instIsLocalRing le_self_add Nat.instCanonicallyOrderedAdd Submodule.finrank_sup_add_finrank_inf_eq FiniteDimensional.finiteDimensional_submodule finrank_add_finrank_orthogonal le_refl IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le instIsDomain instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors Submodule.finiteDimensional_inf_right Disjoint.eq_bot
isCompl_orthogonal_of_restrict_nondegenerate 📖	mathematical	IsRefl Semifield.toCommSemiring Field.toSemifield AddCommGroup.toAddCommMonoid Nondegenerate Submodule CommSemiring.toSemiring SetLike.instMembership Submodule.setLike Submodule.addCommMonoid Submodule.module restrict	IsCompl DivisionSemiring.toSemiring Semifield.toDivisionSemiring Submodule.instPartialOrder CompleteLattice.toBoundedOrder Submodule.completeLattice orthogonal	—	eq_bot_iff Submodule.mem_inf ZeroMemClass.zero_mem IsCompl.of_eq Submodule.eq_top_of_finrank_eq LE.le.antisymm Submodule.finrank_le commRing_strongRankCondition IsLocalRing.toNontrivial Field.instIsLocalRing add_zero finrank_bot Submodule.finrank_sup_add_finrank_inf_eq FiniteDimensional.finiteDimensional_submodule finrank_add_finrank_orthogonal le_self_add Nat.instCanonicallyOrderedAdd
isCompl_span_singleton_orthogonal 📖	mathematical	IsOrtho Semifield.toCommSemiring Field.toSemifield AddCommGroup.toAddCommMonoid	IsCompl Submodule DivisionSemiring.toSemiring Semifield.toDivisionSemiring Submodule.instPartialOrder CompleteLattice.toBoundedOrder Submodule.completeLattice Submodule.span Set Set.instSingletonSet orthogonal	—	LinearMap.isCompl_span_singleton_orthogonal
isOrtho_def 📖	mathematical	—	IsOrtho DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.instFunLike LinearMap.BilinForm LinearMap.addCommMonoid LinearMap.module MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	—
isOrtho_smul_left 📖	mathematical	—	IsOrtho CommRing.toCommSemiring AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Module.toDistribMulAction	—	Algebra.to_smulCommClass map_smul SemilinearMapClass.toMulActionSemiHomClass LinearMap.semilinearMapClass IsDomain.to_noZeroDivisors
isOrtho_smul_right 📖	mathematical	—	IsOrtho CommRing.toCommSemiring AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Module.toDistribMulAction	—	map_smul SemilinearMapClass.toMulActionSemiHomClass LinearMap.semilinearMapClass IsDomain.to_noZeroDivisors
isOrtho_zero_left 📖	mathematical	—	IsOrtho AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	LinearMap.isOrtho_zero_left
isOrtho_zero_right 📖	mathematical	—	IsOrtho AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	zero_right
ker_restrict_eq_of_codisjoint 📖	mathematical	Codisjoint Submodule CommSemiring.toSemiring Submodule.instPartialOrder Submodule.instOrderTop DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.instFunLike LinearMap.BilinForm LinearMap.addCommMonoid LinearMap.module MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	LinearMap.ker SetLike.instMembership Submodule.setLike Submodule.addCommMonoid Submodule.module restrict Submodule.comap Submodule.subtype	—	Submodule.ext LinearMap.ext Submodule.codisjoint_iff_exists_add_eq map_add SemilinearMapClass.toAddHomClass LinearMap.semilinearMapClass add_zero LinearMap.congr_fun
le_orthogonal_orthogonal 📖	mathematical	IsRefl	Submodule CommSemiring.toSemiring Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder orthogonal	—	—
linearIndependent_of_iIsOrtho 📖	mathematical	iIsOrtho Semifield.toCommSemiring Field.toSemifield AddCommGroup.toAddCommMonoid IsOrtho	LinearIndependent DivisionSemiring.toSemiring Semifield.toDivisionSemiring	—	linearIndependent_iff' zero_left Finset.sum_eq_single_of_mem iIsOrtho_def MulZeroClass.mul_zero eq_zero_of_ne_zero_of_mul_right_eq_zero IsDomain.to_noZeroDivisors instIsDomain Finset.sum_congr smul_left sum_left
mem_orthogonal_iff 📖	mathematical	—	Submodule CommSemiring.toSemiring SetLike.instMembership Submodule.setLike orthogonal IsOrtho	—	—
ne_zero_of_not_isOrtho_self 📖	—	IsOrtho Semifield.toCommSemiring Field.toSemifield AddCommGroup.toAddCommMonoid	—	—	isOrtho_zero_left
nondegenerate_restrict_of_disjoint_orthogonal 📖	mathematical	IsRefl CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Disjoint Submodule CommSemiring.toSemiring Submodule.instPartialOrder Submodule.instOrderBot orthogonal	Nondegenerate SetLike.instMembership Submodule.setLike Submodule.addCommMonoid Submodule.module restrict	—	LinearMap.nondegenerate_restrict_of_disjoint_orthogonal
orthogonal_bot 📖	mathematical	—	orthogonal Bot.bot Submodule CommSemiring.toSemiring Submodule.instBot Top.top Submodule.instTop	—	Submodule.ext map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass
orthogonal_eq_bot_iff 📖	mathematical	IsRefl Semifield.toCommSemiring Field.toSemifield AddCommGroup.toAddCommMonoid Nondegenerate Submodule CommSemiring.toSemiring SetLike.instMembership Submodule.setLike Submodule.addCommMonoid Submodule.module restrict	orthogonal Bot.bot Submodule.instBot Top.top DivisionSemiring.toSemiring Semifield.toDivisionSemiring Submodule.instTop	—	eq_top_of_restrict_nondegenerate_of_orthogonal_eq_bot eq_bot_iff
orthogonal_eq_top_iff 📖	mathematical	IsRefl Semifield.toCommSemiring Field.toSemifield AddCommGroup.toAddCommMonoid Nondegenerate Submodule CommSemiring.toSemiring SetLike.instMembership Submodule.setLike Submodule.addCommMonoid Submodule.module restrict	orthogonal Top.top Submodule.instTop Bot.bot DivisionSemiring.toSemiring Semifield.toDivisionSemiring Submodule.instBot	—	IsCompl.inf_eq_bot isCompl_orthogonal_of_restrict_nondegenerate inf_top_eq orthogonal_bot
orthogonal_le 📖	mathematical	Submodule CommSemiring.toSemiring Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder	orthogonal	—	—
orthogonal_orthogonal 📖	mathematical	Nondegenerate Semifield.toCommSemiring Field.toSemifield AddCommGroup.toAddCommMonoid IsRefl	orthogonal	—	Submodule.eq_of_le_of_finrank_le FiniteDimensional.finiteDimensional_submodule le_orthogonal_orthogonal finrank_orthogonal
orthogonal_span_singleton_eq_toLin_ker 📖	mathematical	—	orthogonal Semifield.toCommSemiring Field.toSemifield AddCommGroup.toAddCommMonoid Submodule.span DivisionSemiring.toSemiring Semifield.toDivisionSemiring Set Set.instSingletonSet LinearMap.ker CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.id toLinHomAux₁	—	LinearMap.orthogonal_span_singleton_eq_to_lin_ker
orthogonal_top_eq_bot 📖	mathematical	Nondegenerate IsRefl	orthogonal Top.top Submodule CommSemiring.toSemiring Submodule.instTop Bot.bot Submodule.instBot	—	Submodule.eq_bot_iff Submodule.mem_top
orthogonal_top_eq_ker 📖	mathematical	IsRefl	orthogonal Top.top Submodule CommSemiring.toSemiring Submodule.instTop LinearMap.ker LinearMap RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.addCommMonoid LinearMap.module	—	Submodule.ext smulCommClass_self LinearMap.IsRefl.eq_iff
restrict_nondegenerate_iff_isCompl_orthogonal 📖	mathematical	IsRefl Semifield.toCommSemiring Field.toSemifield AddCommGroup.toAddCommMonoid	Nondegenerate Submodule CommSemiring.toSemiring SetLike.instMembership Submodule.setLike Submodule.addCommMonoid Submodule.module restrict IsCompl DivisionSemiring.toSemiring Semifield.toDivisionSemiring Submodule.instPartialOrder CompleteLattice.toBoundedOrder Submodule.completeLattice orthogonal	—	isCompl_orthogonal_of_restrict_nondegenerate nondegenerate_restrict_of_disjoint_orthogonal IsCompl.disjoint
restrict_nondegenerate_orthogonal_spanSingleton 📖	mathematical	Nondegenerate Semifield.toCommSemiring Field.toSemifield AddCommGroup.toAddCommMonoid IsRefl IsOrtho	Submodule CommSemiring.toSemiring SetLike.instMembership Submodule.setLike orthogonal Submodule.span DivisionSemiring.toSemiring Semifield.toDivisionSemiring Set Set.instSingletonSet Submodule.addCommMonoid Submodule.module restrict	—	Submodule.mem_top span_singleton_sup_orthogonal_eq_top Submodule.coe_eq_zero Submodule.mem_sup add_right add_zero add_left
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 orthogonal Bot.bot Submodule.instBot	—	LinearMap.span_singleton_inf_orthogonal_eq_bot
span_singleton_sup_orthogonal_eq_top 📖	mathematical	IsOrtho Semifield.toCommSemiring Field.toSemifield AddCommGroup.toAddCommMonoid	Submodule DivisionSemiring.toSemiring Semifield.toDivisionSemiring SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Submodule.completeLattice Submodule.span Set Set.instSingletonSet orthogonal Top.top Submodule.instTop	—	LinearMap.span_singleton_sup_orthogonal_eq_top
toLin_restrict_ker_eq_inf_orthogonal 📖	mathematical	IsRefl Semifield.toCommSemiring Field.toSemifield AddCommGroup.toAddCommMonoid	Submodule.map Submodule DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring Field.toDivisionRing SetLike.instMembership Submodule.setLike Submodule.addCommMonoid Submodule.module RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids Submodule.subtype LinearMap.ker CommSemiring.toSemiring LinearMap NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.addCommMonoid LinearMap.module LinearMap.domRestrict Subspace Submodule.instMin orthogonal Top.top Submodule.instTop	—	Submodule.ext RingHomSurjective.ids IsOrtho.eq_1 LinearMap.ext Submodule.mem_top
toLin_restrict_range_dualCoannihilator_eq_orthogonal 📖	mathematical	—	Submodule.dualCoannihilator Semifield.toCommSemiring Field.toSemifield AddCommGroup.toAddCommMonoid LinearMap.range Submodule CommSemiring.toSemiring SetLike.instMembership Submodule.setLike LinearMap RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule Submodule.addCommMonoid LinearMap.addCommMonoid Submodule.module LinearMap.module RingHomSurjective.ids LinearMap.domRestrict orthogonal	—	Submodule.ext RingHomSurjective.ids mem_orthogonal_iff smulCommClass_self Submodule.mem_dualCoannihilator

LinearMap.BilinForm.IsAlt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ortho_comm 📖	mathematical	LinearMap.BilinForm.IsAlt CommRing.toCommSemiring AddCommGroup.toAddCommMonoid	LinearMap.BilinForm.IsOrtho	—	LinearMap.IsAlt.ortho_comm

LinearMap.BilinForm.IsRefl

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ortho_comm 📖	mathematical	LinearMap.BilinForm.IsRefl	LinearMap.BilinForm.IsOrtho	—	eq_zero

LinearMap.BilinForm.IsSymm

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ortho_comm 📖	mathematical	LinearMap.BilinForm.IsSymm	LinearMap.BilinForm.IsOrtho	—	LinearMap.IsSymm.ortho_comm LinearMap.BilinForm.isSymm_iff

LinearMap.BilinForm.iIsOrtho

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
nondegenerate_iff_not_isOrtho_basis_self 📖	mathematical	LinearMap.BilinForm.iIsOrtho DFunLike.coe Module.Basis CommSemiring.toSemiring Module.Basis.instFunLike	LinearMap.BilinForm.Nondegenerate LinearMap.BilinForm.IsOrtho	—	not_isOrtho_basis_self_of_nondegenerate LinearMap.IsOrthoᵢ.nondegenerate_of_not_isOrtho_basis_self instIsTorsionFree
not_isOrtho_basis_self_of_nondegenerate 📖	mathematical	LinearMap.BilinForm.iIsOrtho DFunLike.coe Module.Basis CommSemiring.toSemiring Module.Basis.instFunLike LinearMap.BilinForm.Nondegenerate	LinearMap.BilinForm.IsOrtho	—	LinearMap.IsOrthoᵢ.not_isOrtho_basis_self_of_separatingLeft

---

← Back to Index