Documentation Verification Report

IsBaseChangeFree

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

Statistics

Metric	Count
Definitions `basis`	1
Theorems `basis_apply`, `basis_repr_comp`, `basis_repr_comp_apply`, `free`, `of_basis`, `of_fintype_basis`, `of_fintype_basis_eq`	7
Total	8

IsBaseChange

Definitions

Name	Category	Theorems
`basis` 📖	CompOp	5 math math: `basis_repr_comp_apply`, `endHom_toMatrix`, `linearMapLeftRightHom_toMatrix`, `basis_apply`, `basis_repr_comp`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`basis_apply` 📖	mathematical	`IsBaseChange`	`DFunLike.coe` `Module.Basis` `CommSemiring.toSemiring` `Module.Basis.instFunLike` `basis` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.instFunLike`	—	`RingHomInvPair.ids` `Algebra.to_smulCommClass` `LinearMap.map_zero` `Finsupp.mapRange_single` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `one_smul` `Module.Basis.repr_symm_apply` `Finsupp.linearCombination_single` `IsScalarTower.right`
`basis_repr_comp` 📖	mathematical	`IsBaseChange`	`DFunLike.coe` `LinearEquiv` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Finsupp.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Finsupp.module` `Semiring.toModule` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `Module.Basis.repr` `basis` `LinearMap` `LinearMap.instFunLike` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Algebra.toModule` `Finsupp.mapRange.linearMap` `Algebra.linearMap`	—	`Finsupp.ext` `RingHomInvPair.ids` `basis_repr_comp_apply`
`basis_repr_comp_apply` 📖	mathematical	`IsBaseChange`	`DFunLike.coe` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Finsupp.instFunLike` `LinearEquiv` `RingHom.id` `RingHomInvPair.ids` `Finsupp.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Finsupp.module` `Semiring.toModule` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `Module.Basis.repr` `basis` `LinearMap` `LinearMap.instFunLike` `RingHom` `RingHom.instFunLike` `algebraMap`	—	`RingHomInvPair.ids` `Module.Basis.linearCombination_repr` `Finsupp.linearCombination_apply` `map_finsuppSum` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `SemilinearEquivClass.instSemilinearMapClass` `LinearEquiv.instSemilinearEquivClass` `map_smul` `SemilinearMapClass.toMulActionSemiHomClass` `Finsupp.sum_apply` `Finsupp.sum_eq_single` `IsScalarTower.algebraMap_smul` `basis_apply` `Module.Basis.repr_self` `algebraMap_smul` `Finsupp.isScalarTower` `IsScalarTower.right` `Finsupp.smul_single` `Finsupp.single_eq_of_ne` `zero_smul` `map_zero` `AddMonoidHomClass.toZeroHomClass` `Algebra.algebraMap_eq_smul_one` `smul_assoc` `one_smul` `Finsupp.single_eq_same`
`free` 📖	mathematical	`IsBaseChange`	`Module.Free` `CommSemiring.toSemiring`	—	`Module.Free.of_basis`
`of_basis` 📖	mathematical	—	`IsBaseChange` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Finsupp.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Finsupp.module` `Semiring.toModule` `Finsupp.linearCombination` `DFunLike.coe` `Module.Basis` `Module.Basis.instFunLike`	—	`RingHomInvPair.ids` `IsScalarTower.to_smulCommClass` `IsScalarTower.right` `of_equiv` `Algebra.to_smulCommClass` `RingHomCompTriple.ids` `LinearMap.coe_comp` `LinearEquiv.coe_toLinearMap` `Function.Bijective.of_comp_iff` `LinearEquiv.bijective` `Module.Basis.linearIndependent` `Module.Basis.span_eq` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `Finsupp.ext` `TensorProduct.finsuppScalarRight_apply_tmul_apply` `Algebra.algebraMap_eq_smul_one` `Finsupp.sum_mapRange_index` `zero_smul` `algebraMap_smul`
`of_fintype_basis` 📖	mathematical	—	`IsBaseChange` `Pi.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Pi.Function.module` `Semiring.toModule` `Fintype.linearCombination` `DFunLike.coe` `Module.Basis` `Module.Basis.instFunLike`	—	`RingHomInvPair.ids` `Algebra.to_smulCommClass` `IsScalarTower.right` `of_equiv` `RingHomCompTriple.ids` `LinearMap.coe_comp` `LinearEquiv.coe_toLinearMap` `Function.Bijective.of_comp_iff` `LinearEquiv.bijective` `Module.Basis.linearIndependent` `Module.Basis.span_eq` `IsScalarTower.to_smulCommClass` `TensorProduct.piScalarRight_apply` `TensorProduct.piScalarRightHom_tmul` `smul_assoc` `one_smul`
`of_fintype_basis_eq` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `Pi.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Pi.Function.module` `Semiring.toModule` `LinearMap.instFunLike` `Fintype.linearCombination` `Module.Basis` `Module.Basis.instFunLike` `RingHom` `RingHom.instFunLike` `algebraMap` `LinearEquiv` `RingHomInvPair.ids` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `Module.Basis.equivFun` `Finite.of_fintype`	—	`RingHomInvPair.ids` `Finite.of_fintype` `LinearEquiv.symm_apply_eq` `Fintype.linearCombination_apply` `Module.Basis.equivFun_symm_apply` `Finset.sum_congr` `algebraMap_smul`

---

← Back to Index