BaseChange

📁 Source: Mathlib/LinearAlgebra/Dual/BaseChange.lean

Statistics

Metric	Count
Definitions toDual, toDualBaseChange, baseChange	3
Theorems dual, toDualBaseChange_tmul, toDual_apply, toDual_comp_apply, baseChange_apply_tmul, baseChange_baseChange, congr_apply_apply, congr_symm_apply_apply	8
Total	11

IsBaseChange

Definitions

Name	Category	Theorems
toDual 📖	CompOp	4 math math: transvection, toDual_comp_apply, toDual_apply, dual
toDualBaseChange 📖	CompOp	1 math math: toDualBaseChange_tmul

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
dual 📖	mathematical	IsBaseChange	Module.Dual CommSemiring.toSemiring LinearMap.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.id LinearMap.module Algebra.to_smulCommClass Algebra.id Algebra.toModule IsScalarTower.to_smulCommClass' IsScalarTower.right LinearMap.instIsScalarTower DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid Module.toDistribMulAction Algebra.toSMul toDual	—	of_equiv Algebra.to_smulCommClass IsScalarTower.to_smulCommClass' IsScalarTower.right LinearMap.instIsScalarTower RingHomInvPair.ids smulCommClass_self one_smul LinearMap.instSMulCommClass
toDualBaseChange_tmul 📖	mathematical	IsBaseChange	DFunLike.coe Module.Dual CommSemiring.toSemiring LinearMap.instFunLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.id LinearEquiv RingHomInvPair.ids TensorProduct LinearMap.addCommMonoid Algebra.toModule LinearMap.module Algebra.to_smulCommClass Algebra.id TensorProduct.addCommMonoid TensorProduct.leftModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toDualBaseChange TensorProduct.tmul LinearMap Distrib.toMul NonUnitalNonAssocSemiring.toDistrib RingHom RingHom.instFunLike algebraMap	—	—
toDual_apply 📖	mathematical	IsBaseChange	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring Module.Dual LinearMap.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.module Algebra.to_smulCommClass Algebra.id Algebra.toModule IsScalarTower.to_smulCommClass' IsScalarTower.right LinearMap.instFunLike toDual LinearEquiv RingHomInvPair.ids TensorProduct TensorProduct.addCommMonoid TensorProduct.leftModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv Module.Dual.congr equiv Module.Dual.baseChange	—	algHom_ext Algebra.to_smulCommClass IsScalarTower.to_smulCommClass' IsScalarTower.right RingHomInvPair.ids toDual_comp_apply Algebra.algebraMap_eq_smul_one equiv_symm_apply
toDual_comp_apply 📖	mathematical	IsBaseChange	DFunLike.coe Module.Dual CommSemiring.toSemiring LinearMap.instFunLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.id LinearMap LinearMap.addCommMonoid LinearMap.module Algebra.to_smulCommClass Algebra.id Algebra.toModule IsScalarTower.to_smulCommClass' IsScalarTower.right toDual RingHom RingHom.instFunLike algebraMap	—	Algebra.to_smulCommClass IsScalarTower.to_smulCommClass' IsScalarTower.right linearMapLeftRightHom_comp_apply

Module.Dual

Definitions

Name	Category	Theorems
baseChange 📖	CompOp	4 math math: baseChange_apply_tmul, IsBaseChange.toDual_apply, baseChange_baseChange, LinearMap.transvection.baseChange

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
baseChange_apply_tmul 📖	mathematical	—	DFunLike.coe Module.Dual TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Algebra.toModule TensorProduct.addCommMonoid TensorProduct.leftModule Semiring.toModule Algebra.to_smulCommClass LinearMap.instFunLike RingHom.id LinearMap LinearMap.addCommMonoid LinearMap.module Algebra.id IsScalarTower.to_smulCommClass' IsScalarTower.right baseChange TensorProduct.tmul Algebra.toSMul	—	Algebra.to_smulCommClass IsScalarTower.to_smulCommClass' IsScalarTower.right
baseChange_baseChange 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring Module.Dual TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Algebra.toModule TensorProduct.addCommMonoid TensorProduct.leftModule Semiring.toModule Algebra.to_smulCommClass LinearMap.addCommMonoid LinearMap.module Algebra.id IsScalarTower.to_smulCommClass' IsScalarTower.right LinearMap.instFunLike baseChange LinearEquiv RingHomInvPair.ids IsScalarTower.to_smulCommClass EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv LinearEquiv.symm congr TensorProduct.AlgebraTensorModule.cancelBaseChange	—	TensorProduct.AlgebraTensorModule.curry_injective IsScalarTower.right Algebra.to_smulCommClass IsScalarTower.to_smulCommClass' RingHomInvPair.ids IsScalarTower.to_smulCommClass LinearMap.ext_ring LinearMap.ext smul_assoc one_smul
congr_apply_apply 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.instFunLike LinearEquiv RingHomInvPair.ids Module.Dual LinearMap.addCommMonoid LinearMap.module Algebra.to_smulCommClass Algebra.id EquivLike.toFunLike LinearEquiv.instEquivLike congr LinearEquiv.symm	—	RingHomInvPair.ids Algebra.to_smulCommClass
congr_symm_apply_apply 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.instFunLike LinearEquiv RingHomInvPair.ids Module.Dual LinearMap.addCommMonoid LinearMap.module Algebra.to_smulCommClass Algebra.id EquivLike.toFunLike LinearEquiv.instEquivLike LinearEquiv.symm congr	—	RingHomInvPair.ids Algebra.to_smulCommClass

---

← Back to Index