IsBaseChangeHom

📁 Source: Mathlib/RingTheory/TensorProduct/IsBaseChangeHom.lean

Statistics

Metric	Count
Definitions endHom, linearMapLeftRightHom, linearMapRightBaseChangeEquiv, linearMapRightBaseChangeHom	4
Theorems det_endHom, end, endHom_apply, endHom_comp, endHom_comp_apply, endHom_one, endHom_toMatrix, linearMapLeftRight, linearMapLeftRightHom_apply, linearMapLeftRightHom_comp, linearMapLeftRightHom_comp_apply, linearMapLeftRightHom_toMatrix, linearMapRight	13
Total	17

IsBaseChange

Definitions

Name	Category	Theorems
endHom 📖	CompOp	8 math math: endHom_toMatrix, transvection, det_endHom, end, endHom_apply, endHom_one, endHom_comp_apply, endHom_comp
linearMapLeftRightHom 📖	CompOp	5 math math: linearMapLeftRightHom_comp_apply, linearMapLeftRightHom_toMatrix, linearMapLeftRight, linearMapLeftRightHom_apply, linearMapLeftRightHom_comp
linearMapRightBaseChangeEquiv 📖	CompOp	—
linearMapRightBaseChangeHom 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
det_endHom 📖	mathematical	IsBaseChange AddCommGroup.toAddCommMonoid CommRing.toCommSemiring	DFunLike.coe MonoidHom LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring MonoidHom.instFunLike LinearMap.det LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction IsScalarTower.to_smulCommClass' LinearMap.instFunLike endHom RingHom RingHom.instFunLike algebraMap	—	smulCommClass_self IsScalarTower.to_smulCommClass' subsingleton_or_nontrivial Module.subsingleton Subsingleton.eq_one Unique.instSubsingleton endHom_one map_one MonoidHomClass.toOneHomClass MonoidHom.instMonoidHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass commRing_strongRankCondition RingHomInvPair.ids Finite.of_fintype LinearMap.det_toMatrix endHom_toMatrix RingHom.mapMatrix_apply RingHom.map_det
end 📖	mathematical	IsBaseChange	LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction IsScalarTower.to_smulCommClass' LinearMap.instIsScalarTower DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Algebra.toSMul endHom	—	of_equiv smulCommClass_self IsScalarTower.to_smulCommClass' LinearMap.instIsScalarTower Algebra.to_smulCommClass RingHomCompTriple.ids RingHomInvPair.ids IsScalarTower.to_smulCommClass LinearMap.IsScalarTower.compatibleSMul IsScalarTower.left linearMapRight LinearMap.ext one_smul endHom_apply
endHom_apply 📖	mathematical	IsBaseChange	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction IsScalarTower.to_smulCommClass' endHom TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Algebra.toModule TensorProduct.addCommMonoid TensorProduct.leftModule Semiring.toModule Algebra.to_smulCommClass LinearEquiv RingHomInvPair.ids IsScalarTower.to_smulCommClass EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv LinearMap.liftBaseChangeEquiv LinearMap.comp RingHomCompTriple.ids LinearEquiv.symm equiv	—	smulCommClass_self IsScalarTower.to_smulCommClass'
endHom_comp 📖	mathematical	IsBaseChange	LinearMap.comp CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids LinearMap.restrictScalars LinearMap.IsScalarTower.compatibleSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Algebra.toSMul DFunLike.coe LinearMap LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid IsScalarTower.to_smulCommClass' LinearMap.instFunLike endHom	—	LinearMap.ext RingHomCompTriple.ids LinearMap.IsScalarTower.compatibleSMul smulCommClass_self IsScalarTower.to_smulCommClass' endHom_comp_apply
endHom_comp_apply 📖	mathematical	IsBaseChange	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction IsScalarTower.to_smulCommClass' endHom	—	smulCommClass_self IsScalarTower.to_smulCommClass' Algebra.to_smulCommClass RingHomInvPair.ids IsScalarTower.to_smulCommClass RingHomCompTriple.ids endHom_apply equiv_symm_apply one_smul
endHom_one 📖	mathematical	IsBaseChange	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction IsScalarTower.to_smulCommClass' LinearMap.instFunLike endHom Module.End.instOne	—	LinearMap.ext smulCommClass_self IsScalarTower.to_smulCommClass' inductionOn map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass endHom_comp_apply map_smul SemilinearMapClass.toMulActionSemiHomClass map_add SemilinearMapClass.toAddHomClass
endHom_toMatrix 📖	mathematical	IsBaseChange	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearMap Matrix LinearMap.addCommMonoid Matrix.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Matrix.module Semiring.toModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv LinearMap.toMatrix Finite.of_fintype basis IsScalarTower.to_smulCommClass' LinearMap.instFunLike endHom Matrix.map RingHom RingHom.instFunLike algebraMap	—	Matrix.ext RingHomInvPair.ids smulCommClass_self Finite.of_fintype IsScalarTower.to_smulCommClass' LinearMap.toMatrix_apply basis_apply endHom_comp_apply basis_repr_comp_apply
linearMapLeftRight 📖	mathematical	IsBaseChange	LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction IsScalarTower.to_smulCommClass' LinearMap.instIsScalarTower DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Algebra.toSMul linearMapLeftRightHom	—	of_equiv smulCommClass_self IsScalarTower.to_smulCommClass' LinearMap.instIsScalarTower Algebra.to_smulCommClass RingHomCompTriple.ids RingHomInvPair.ids IsScalarTower.to_smulCommClass LinearMap.IsScalarTower.compatibleSMul IsScalarTower.left linearMapRight LinearMap.ext one_smul linearMapLeftRightHom_apply
linearMapLeftRightHom_apply 📖	mathematical	IsBaseChange	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction IsScalarTower.to_smulCommClass' linearMapLeftRightHom TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Algebra.toModule TensorProduct.addCommMonoid TensorProduct.leftModule Semiring.toModule Algebra.to_smulCommClass LinearEquiv RingHomInvPair.ids IsScalarTower.to_smulCommClass EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv LinearMap.liftBaseChangeEquiv LinearMap.comp RingHomCompTriple.ids LinearEquiv.symm equiv	—	smulCommClass_self IsScalarTower.to_smulCommClass'
linearMapLeftRightHom_comp 📖	mathematical	IsBaseChange	LinearMap.comp CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids LinearMap.restrictScalars LinearMap.IsScalarTower.compatibleSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Algebra.toSMul DFunLike.coe LinearMap LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid IsScalarTower.to_smulCommClass' LinearMap.instFunLike linearMapLeftRightHom	—	LinearMap.ext RingHomCompTriple.ids LinearMap.IsScalarTower.compatibleSMul smulCommClass_self IsScalarTower.to_smulCommClass' linearMapLeftRightHom_comp_apply
linearMapLeftRightHom_comp_apply 📖	mathematical	IsBaseChange	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction IsScalarTower.to_smulCommClass' linearMapLeftRightHom	—	smulCommClass_self IsScalarTower.to_smulCommClass' Algebra.to_smulCommClass RingHomInvPair.ids IsScalarTower.to_smulCommClass RingHomCompTriple.ids linearMapLeftRightHom_apply equiv_symm_apply one_smul
linearMapLeftRightHom_toMatrix 📖	mathematical	IsBaseChange	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearMap Matrix LinearMap.addCommMonoid Matrix.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Matrix.module Semiring.toModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv LinearMap.toMatrix basis IsScalarTower.to_smulCommClass' LinearMap.instFunLike linearMapLeftRightHom Matrix.map RingHom RingHom.instFunLike algebraMap	—	Matrix.ext RingHomInvPair.ids smulCommClass_self IsScalarTower.to_smulCommClass' LinearMap.toMatrix_apply basis_apply linearMapLeftRightHom_comp_apply basis_repr_comp_apply
linearMapRight 📖	mathematical	IsBaseChange	LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction IsScalarTower.to_smulCommClass LinearMap.instIsScalarTower DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Algebra.toSMul LinearMap.compRight LinearMap.IsScalarTower.compatibleSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass Algebra.id IsScalarTower.left	—	of_equiv smulCommClass_self IsScalarTower.to_smulCommClass LinearMap.instIsScalarTower LinearMap.IsScalarTower.compatibleSMul IsScalarTower.left RingHomInvPair.ids Algebra.to_smulCommClass RingHomCompTriple.ids one_smul LinearMap.instSMulCommClass

---

← Back to Index