Basic

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

Statistics

Metric	Count
Definitions coeFnAddMonoidHom, flip, flipHom, restrict	4
Theorems add_apply, add_left, add_right, coeFnAddMonoidHom_apply, coe_injective, congr_fun, ext, ext_iff, flip_apply, flip_flip, neg_apply, neg_left, neg_right, restrict_apply, smul_left, smul_left_of_tower, smul_right, smul_right_of_tower, sub_apply, sub_left, sub_right, zero_apply, zero_left, zero_right, lsmul_flip_apply	25
Total	29

LinearMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
lsmul_flip_apply 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule 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 instFunLike flip lsmul toSpanSingleton	—	SMulCommClass.symm smulCommClass_self

LinearMap.BilinForm

Definitions

Name	Category	Theorems
coeFnAddMonoidHom 📖	CompOp	1 math math: coeFnAddMonoidHom_apply
flip 📖	CompOp	8 math math: nondegenerate_flip_iff, dualSubmodule_dualSubmodule_flip_of_basis, Nondegenerate.flip, dualSubmodule_flip_dualSubmodule_of_basis, nonDegenerateFlip_iff, dualBasis_dualBasis_flip, le_flip_dualSubmodule, dualBasis_flip_dualBasis
flipHom 📖	CompOp	3 math math: isSymm_iff_flip, flip_apply, flip_flip
restrict 📖	CompOp	20 math math: RootPairing.rootForm_restrict_nondegenerate_of_ordered, LieAlgebra.IsKilling.restrict_killingForm_eq_sum, ker_restrict_eq_of_codisjoint, LieIdeal.restrict_killingForm, restrict_nondegenerate_iff_isCompl_orthogonal, restrict_nondegenerate_orthogonal_spanSingleton, LieAlgebra.InvariantForm.restrict_nondegenerate, LieSubmodule.traceForm_eq_of_le_idealizer, LieDerivation.IsKilling.killingForm_restrict_range_ad, inf_orthogonal_self_le_ker_restrict, LieAlgebra.IsKilling.corootForm_rootSystem_eq_killing, LieAlgebra.InvariantForm.restrict_orthogonal_nondegenerate, LieIdeal.killingForm_eq, LieAlgebra.restrict_killingForm, IsSymm.restrict, RootPairing.rootForm_restrict_nondegenerate_of_isAnisotropic, LieAlgebra.IsKilling.ker_restrict_eq_bot_of_isCartanSubalgebra, LieDerivation.IsKilling.killingForm_restrict_range_ad_nondegenerate, restrict_apply, nondegenerate_restrict_of_disjoint_orthogonal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add_apply 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.instFunLike LinearMap.BilinForm LinearMap.addCommMonoid LinearMap.module LinearMap.instAdd Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib	—	—
add_left 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.instFunLike LinearMap.BilinForm LinearMap.addCommMonoid LinearMap.module AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib	—	LinearMap.map_add₂
add_right 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.instFunLike LinearMap.BilinForm LinearMap.addCommMonoid LinearMap.module AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib	—	map_add SemilinearMapClass.toAddHomClass LinearMap.semilinearMapClass
coeFnAddMonoidHom_apply 📖	mathematical	—	DFunLike.coe AddMonoidHom LinearMap.BilinForm AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid LinearMap.addCommMonoid LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.module Pi.addZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne AddMonoidHom.instFunLike coeFnAddMonoidHom LinearMap.instFunLike	—	—
coe_injective 📖	mathematical	—	LinearMap.BilinForm DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module	—	LinearMap.ext
congr_fun 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.instFunLike LinearMap.BilinForm LinearMap.addCommMonoid LinearMap.module	—	LinearMap.congr_fun₂
ext 📖	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.instFunLike LinearMap.BilinForm LinearMap.addCommMonoid LinearMap.module	—	—	LinearMap.ext₂
ext_iff 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.instFunLike LinearMap.BilinForm LinearMap.addCommMonoid LinearMap.module	—	ext
flip_apply 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.instFunLike LinearMap.BilinForm LinearMap.addCommMonoid LinearMap.module LinearEquiv RingHomInvPair.ids Algebra.to_smulCommClass Algebra.id LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid Module.toDistribMulAction EquivLike.toFunLike LinearEquiv.instEquivLike flipHom	—	RingHomInvPair.ids Algebra.to_smulCommClass LinearMap.instSMulCommClass
flip_flip 📖	mathematical	—	LinearEquiv.trans LinearMap.BilinForm CommSemiring.toSemiring LinearMap.addCommMonoid LinearMap RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.module Algebra.to_smulCommClass Algebra.id LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid Module.toDistribMulAction RingHomCompTriple.ids RingHomInvPair.ids flipHom LinearEquiv.refl	—	LinearEquiv.ext Algebra.to_smulCommClass LinearMap.instSMulCommClass RingHomInvPair.ids RingHomCompTriple.ids ext
neg_apply 📖	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 LinearMap.instNeg LinearMap.addCommGroup Ring.toAddCommGroup CommRing.toRing NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	—
neg_left 📖	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 NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup CommRing.toRing	—	LinearMap.map_neg₂
neg_right 📖	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 NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup CommRing.toRing	—	map_neg DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass
restrict_apply 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring Submodule SetLike.instMembership Submodule.setLike Submodule.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Submodule.module Semiring.toModule LinearMap.addCommMonoid LinearMap.module LinearMap.instFunLike restrict LinearMap.domRestrict	—	—
smul_left 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.instFunLike LinearMap.BilinForm LinearMap.addCommMonoid LinearMap.module SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	LinearMap.map_smul₂
smul_left_of_tower 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.instFunLike LinearMap.BilinForm LinearMap.addCommMonoid LinearMap.module SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Algebra.toSMul	—	IsScalarTower.algebraMap_smul smul_left Algebra.smul_def
smul_right 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.instFunLike LinearMap.BilinForm LinearMap.addCommMonoid LinearMap.module SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	map_smul SemilinearMapClass.toMulActionSemiHomClass LinearMap.semilinearMapClass
smul_right_of_tower 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.instFunLike LinearMap.BilinForm LinearMap.addCommMonoid LinearMap.module SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Algebra.toSMul	—	IsScalarTower.algebraMap_smul smul_right Algebra.smul_def
sub_apply 📖	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 LinearMap.instSub LinearMap.addCommGroup Ring.toAddCommGroup CommRing.toRing SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne	—	—
sub_left 📖	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 AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing	—	LinearMap.map_sub₂
sub_right 📖	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 AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing	—	map_sub DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass
zero_apply 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.instFunLike LinearMap.BilinForm LinearMap.addCommMonoid LinearMap.module LinearMap.instZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	—
zero_left 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.instFunLike LinearMap.BilinForm LinearMap.addCommMonoid LinearMap.module AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	LinearMap.map_zero₂
zero_right 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.instFunLike LinearMap.BilinForm LinearMap.addCommMonoid LinearMap.module AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass

---

← Back to Index