Hom

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

Statistics

Metric	Count
Definitions congrRight₂, comp, compLeft, compRight, linMulLin, toLinHomAux₁, toLinHomFlip, compBilinForm	8
Theorems congrRight_symm, congrRight₂_apply, congrRight₂_refl, congrRight₂_trans, compLeft_apply, compLeft_compRight, compLeft_id, compRight_apply, compRight_compLeft, compRight_id, comp_apply, comp_comp, comp_congr, comp_id_id, comp_id_left, comp_id_right, comp_inj, congr_apply, congr_comp, congr_congr, congr_refl, congr_symm, congr_trans, ext_basis, linMulLin_apply, linMulLin_comp, linMulLin_compLeft, linMulLin_compRight, sum_apply, sum_left, sum_repr_mul_repr_mul, sum_right, toLin'Flip_apply, compBilinForm_apply_apply	34
Total	42

LinearEquiv

Definitions

Name	Category	Theorems
congrRight₂ 📖	CompOp	4 math math: congrRight₂_refl, congrRight_symm, congrRight₂_apply, congrRight₂_trans

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congrRight_symm 📖	mathematical	—	symm LinearMap.BilinMap CommSemiring.toSemiring LinearMap.addCommMonoid LinearMap RingHom.id Semiring.toNonAssocSemiring LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero RingHomInvPair.ids congrRight₂	—	RingHomInvPair.ids smulCommClass_self LinearMap.instSMulCommClass
congrRight₂_apply 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearMap.BilinMap LinearMap.addCommMonoid LinearMap LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero EquivLike.toFunLike instEquivLike congrRight₂ LinearMap.compr₂ Semiring.toModule IsScalarTower.left toLinearMap	—	RingHomInvPair.ids smulCommClass_self LinearMap.instSMulCommClass
congrRight₂_refl 📖	mathematical	—	congrRight₂ refl CommSemiring.toSemiring LinearMap.BilinMap LinearMap.addCommMonoid LinearMap RingHom.id Semiring.toNonAssocSemiring LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	RingHomInvPair.ids smulCommClass_self LinearMap.instSMulCommClass
congrRight₂_trans 📖	mathematical	—	congrRight₂ trans CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids RingHomInvPair.ids LinearMap.BilinMap LinearMap.addCommMonoid LinearMap LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	RingHomInvPair.ids smulCommClass_self LinearMap.instSMulCommClass RingHomCompTriple.ids

LinearMap

Definitions

Name	Category	Theorems
compBilinForm 📖	CompOp	1 math math: compBilinForm_apply_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
compBilinForm_apply_apply 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule instFunLike addCommMonoid module compBilinForm Algebra.toModule	—	—

LinearMap.BilinForm

Definitions

Name	Category	Theorems
comp 📖	CompOp	19 math math: comp_id_right, linMulLin_comp, congr_comp, mul_toMatrix'_mul, BilinForm.mul_toMatrix_mul, comp_inj, comp_id_left, BilinForm.toMatrix_comp, compRight_compLeft, compLeft_compRight, comp_id_id, comp_congr, Matrix.toBilin'_comp, mul_toMatrix_mul, toMatrix'_comp, comp_comp, comp_apply, toMatrix_comp, Matrix.toBilin_comp
compLeft 📖	CompOp	13 math math: comp_id_right, compLeft_injective, compRight_compLeft, compLeft_compRight, toMatrix'_compLeft, mul_toMatrix', compLeft_id, toMatrix_compLeft, mul_toMatrix, compLeft_apply, BilinForm.mul_toMatrix, linMulLin_compLeft, BilinForm.toMatrix_compLeft
compRight 📖	CompOp	12 math math: linMulLin_compRight, toMatrix_compRight, comp_id_left, compRight_compLeft, compLeft_compRight, compRight_id, BilinForm.toMatrix_compRight, compRight_apply, toMatrix_mul, BilinForm.toMatrix_mul, toMatrix'_mul, toMatrix'_compRight
linMulLin 📖	CompOp	4 math math: linMulLin_compRight, linMulLin_comp, linMulLin_compLeft, linMulLin_apply
toLinHomAux₁ 📖	CompOp	1 math math: orthogonal_span_singleton_eq_toLin_ker
toLinHomFlip 📖	CompOp	1 math math: toLin'Flip_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
compLeft_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 compLeft	—	—
compLeft_compRight 📖	mathematical	—	compRight compLeft comp	—	—
compLeft_id 📖	mathematical	—	compLeft LinearMap.id CommSemiring.toSemiring	—	ext
compRight_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 compRight	—	—
compRight_compLeft 📖	mathematical	—	compLeft compRight comp	—	—
compRight_id 📖	mathematical	—	compRight LinearMap.id CommSemiring.toSemiring	—	ext
comp_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 comp	—	—
comp_comp 📖	mathematical	—	comp LinearMap.comp CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids	—	—
comp_congr 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearMap.BilinForm LinearMap.addCommMonoid LinearMap 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 EquivLike.toFunLike LinearEquiv.instEquivLike congr comp LinearMap.comp RingHomCompTriple.ids LinearEquiv.toLinearMap LinearEquiv.symm	—	RingHomInvPair.ids Algebra.to_smulCommClass LinearMap.instSMulCommClass
comp_id_id 📖	mathematical	—	comp LinearMap.id CommSemiring.toSemiring	—	ext
comp_id_left 📖	mathematical	—	comp LinearMap.id CommSemiring.toSemiring compRight	—	ext
comp_id_right 📖	mathematical	—	comp LinearMap.id CommSemiring.toSemiring compLeft	—	ext
comp_inj 📖	mathematical	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike	comp	—	ext comp_apply
congr_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 congr LinearEquiv.symm	—	RingHomInvPair.ids Algebra.to_smulCommClass LinearMap.instSMulCommClass
congr_comp 📖	mathematical	—	comp DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearMap.BilinForm LinearMap.addCommMonoid LinearMap 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 EquivLike.toFunLike LinearEquiv.instEquivLike congr LinearMap.comp RingHomCompTriple.ids LinearEquiv.toLinearMap LinearEquiv.symm	—	RingHomInvPair.ids Algebra.to_smulCommClass LinearMap.instSMulCommClass
congr_congr 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearMap.BilinForm LinearMap.addCommMonoid LinearMap 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 EquivLike.toFunLike LinearEquiv.instEquivLike congr LinearEquiv.trans RingHomCompTriple.ids	—	RingHomInvPair.ids Algebra.to_smulCommClass LinearMap.instSMulCommClass
congr_refl 📖	mathematical	—	congr LinearEquiv.refl CommSemiring.toSemiring LinearMap.BilinForm 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	—	LinearEquiv.ext Algebra.to_smulCommClass LinearMap.instSMulCommClass RingHomInvPair.ids LinearMap.ext₂
congr_symm 📖	mathematical	—	LinearEquiv.symm 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 RingHomInvPair.ids congr	—	RingHomInvPair.ids Algebra.to_smulCommClass LinearMap.instSMulCommClass
congr_trans 📖	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 congr	—	RingHomInvPair.ids Algebra.to_smulCommClass LinearMap.instSMulCommClass RingHomCompTriple.ids
ext_basis 📖	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.instFunLike LinearMap.BilinForm LinearMap.addCommMonoid LinearMap.module Module.Basis Module.Basis.instFunLike	—	—	Module.Basis.ext
linMulLin_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 linMulLin Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	—
linMulLin_comp 📖	mathematical	—	comp linMulLin LinearMap.comp CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.id RingHomCompTriple.ids	—	—
linMulLin_compLeft 📖	mathematical	—	compLeft linMulLin LinearMap.comp CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.id RingHomCompTriple.ids	—	—
linMulLin_compRight 📖	mathematical	—	compRight linMulLin LinearMap.comp CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.id RingHomCompTriple.ids	—	—
sum_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 Finset.sum	—	LinearMap.coe_sum Finset.sum_apply
sum_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 Finset.sum	—	LinearMap.map_sum₂
sum_repr_mul_repr_mul 📖	mathematical	—	Finsupp.sum MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid DFunLike.coe LinearEquiv RingHom.id RingHomInvPair.ids Finsupp Finsupp.instAddCommMonoid Finsupp.module Semiring.toModule EquivLike.toFunLike LinearEquiv.instEquivLike Module.Basis.repr Algebra.toSMul Algebra.id LinearMap LinearMap.instFunLike LinearMap.BilinForm LinearMap.addCommMonoid LinearMap.module Module.Basis Module.Basis.instFunLike	—	RingHomInvPair.ids Module.Basis.linearCombination_repr Finset.sum_congr sum_left sum_right smul_left smul_right
sum_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 Finset.sum	—	map_sum DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass
toLin'Flip_apply 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module Algebra.to_smulCommClass Algebra.id LinearMap.BilinForm LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid Module.toDistribMulAction toLinHomFlip	—	Algebra.to_smulCommClass LinearMap.instSMulCommClass

---

← Back to Index