Documentation Verification Report

Basic

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

Statistics

Metric	Count
Definitions `FreeProduct`, `FreeTensorAlgebra`, `PowerAlgebra`, `asPowers`, `asPowersEquiv`, `instAlgebra`, `instModuleDirectSum`, `instSemiring`, `lof`, `mkAlgHom`, `of`, `powerAlgebraEquivFreeTensorAlgebra`, `rel`, `rel'`, `ι`, `ι'`, `algEquivQuotAlgEquiv`, `equivQuotEquiv`	18
Theorems `induction_lon`, `identify_one`, `lift_algebraMap`, `lift_apply`, `lift_comp_ι`, `lift_symm_apply`, `lift_unique`, `lof_map_one`, `mul_injections`, `of_def`, `rel_id`, `ι_apply`, `ι_def`	13
Total	31

DirectSum

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`induction_lon` 📖	—	`DirectSum` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instAddCommMonoidDirectSum` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `instModule` `LinearMap.instFunLike` `lof` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	—	—	`induction_on`

LinearAlgebra

Definitions

Name	Category	Theorems
`FreeProduct` 📖	CompOp	9 math math: `FreeProduct.mul_injections`, `FreeProduct.ι_apply`, `FreeProduct.identify_one`, `FreeProduct.ι_def`, `FreeProduct.lift_algebraMap`, `FreeProduct.lift_symm_apply`, `FreeProduct.lift_apply`, `FreeProduct.lift_comp_ι`, `FreeProduct.lof_map_one`

LinearAlgebra.FreeProduct

Definitions

Name	Category	Theorems
`FreeTensorAlgebra` 📖	CompOp	6 math math: `mul_injections`, `ι_apply`, `identify_one`, `rel_id`, `lift_apply`, `lof_map_one`
`PowerAlgebra` 📖	CompOp	—
`asPowers` 📖	CompOp	—
`asPowersEquiv` 📖	CompOp	—
`instAlgebra` 📖	CompOp	9 math math: `mul_injections`, `ι_apply`, `identify_one`, `ι_def`, `lift_algebraMap`, `lift_symm_apply`, `lift_apply`, `lift_comp_ι`, `lof_map_one`
`instModuleDirectSum` 📖	CompOp	7 math math: `mul_injections`, `ι_apply`, `identify_one`, `ι_def`, `rel_id`, `lift_apply`, `lof_map_one`
`instSemiring` 📖	CompOp	9 math math: `mul_injections`, `ι_apply`, `identify_one`, `ι_def`, `lift_algebraMap`, `lift_symm_apply`, `lift_apply`, `lift_comp_ι`, `lof_map_one`
`lof` 📖	CompOp	1 math math: `lof_map_one`
`mkAlgHom` 📖	CompOp	—
`of` 📖	CompOp	1 math math: `of_def`
`powerAlgebraEquivFreeTensorAlgebra` 📖	CompOp	—
`rel` 📖	CompData	6 math math: `mul_injections`, `ι_apply`, `identify_one`, `rel_id`, `lift_apply`, `lof_map_one`
`rel'` 📖	MathDef	—
`ι` 📖	CompOp	4 math math: `ι_def`, `of_def`, `lift_symm_apply`, `lift_comp_ι`
`ι'` 📖	CompOp	4 math math: `mul_injections`, `ι_apply`, `identify_one`, `ι_def`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`identify_one` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `DirectSum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `LinearAlgebra.FreeProduct` `instAddCommMonoidDirectSum` `RingQuot.instAddCommMonoid` `FreeTensorAlgebra` `instSemiringTensorAlgebra` `instModuleDirectSum` `rel` `Algebra.toModule` `instSemiring` `instAlgebra` `LinearMap.instFunLike` `ι'` `DirectSum.instModule` `DirectSum.lof` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `RingQuot.instOne`	—	`DirectSum.instIsScalarTower` `IsScalarTower.left` `RingQuot.mkAlgHom_rel` `rel_id` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass`
`lift_algebraMap` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `LinearAlgebra.FreeProduct` `instSemiring` `instAlgebra` `AlgHom.funLike` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `lift` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `RingHom.instFunLike` `algebraMap`	—	`lift_apply` `AlgHom.commutes`
`lift_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `AlgHom` `LinearAlgebra.FreeProduct` `instSemiring` `instAlgebra` `EquivLike.toFunLike` `Equiv.instEquivLike` `lift` `FreeTensorAlgebra` `instSemiringTensorAlgebra` `DirectSum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instAddCommMonoidDirectSum` `instModuleDirectSum` `instAlgebra` `Algebra.id` `RingQuot` `rel` `RingQuot.instSemiring` `RingQuot.instAlgebra` `RingQuot.liftAlgHom` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Algebra.toModule` `TensorAlgebra` `TensorAlgebra.lift` `DirectSum.toModule` `AlgHom.toLinearMap`	—	—
`lift_comp_ι` 📖	mathematical	—	`AlgHom.comp` `LinearAlgebra.FreeProduct` `instSemiring` `instAlgebra` `DFunLike.coe` `Equiv` `AlgHom` `EquivLike.toFunLike` `Equiv.instEquivLike` `lift` `ι`	—	`AlgHom.ext` `lof_map_one` `ι_def` `RingQuot.liftAlgHom_mkAlgHom_apply` `IsScalarTower.left` `TensorAlgebra.lift_ι_apply` `DirectSum.toModule_lof`
`lift_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `AlgHom` `LinearAlgebra.FreeProduct` `instSemiring` `instAlgebra` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `lift` `AlgHom.comp` `ι`	—	—
`lift_unique` 📖	mathematical	`AlgHom.comp` `LinearAlgebra.FreeProduct` `instSemiring` `instAlgebra` `ι`	`DFunLike.coe` `Equiv` `AlgHom` `EquivLike.toFunLike` `Equiv.instEquivLike` `lift`	—	`RingQuot.ringQuot_ext'` `TensorAlgebra.hom_ext` `DirectSum.linearMap_ext` `IsScalarTower.left` `RingHomCompTriple.ids` `LinearMap.ext` `lof_map_one` `RingQuot.liftAlgHom_mkAlgHom_apply` `TensorAlgebra.lift_ι_apply` `DirectSum.toModule_lof` `ι_def`
`lof_map_one` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearAlgebra.FreeProduct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `RingQuot.instAddCommMonoid` `FreeTensorAlgebra` `instSemiringTensorAlgebra` `DirectSum` `instAddCommMonoidDirectSum` `instModuleDirectSum` `rel` `Algebra.toModule` `instSemiring` `instAlgebra` `LinearMap.instFunLike` `lof` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `RingQuot.instOne`	—	`lof.eq_1` `identify_one`
`mul_injections` 📖	mathematical	—	`LinearAlgebra.FreeProduct` `RingQuot.instMul` `FreeTensorAlgebra` `instSemiringTensorAlgebra` `DirectSum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instAddCommMonoidDirectSum` `instModuleDirectSum` `rel` `DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `RingQuot.instAddCommMonoid` `Algebra.toModule` `instSemiring` `instAlgebra` `LinearMap.instFunLike` `ι'` `DirectSum.instModule` `DirectSum.lof` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`IsScalarTower.left` `mul_one` `map_mul` `NonUnitalAlgSemiHomClass.toMulHomClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `AlgHom.algHomClass` `RingQuot.mkAlgHom_rel`
`of_def` 📖	mathematical	—	`of` `ι`	—	—
`rel_id` 📖	mathematical	—	`rel` `DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `DirectSum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `TensorAlgebra` `instAddCommMonoidDirectSum` `instModuleDirectSum` `instSemiringTensorAlgebra` `Algebra.toModule` `instAlgebra` `Algebra.id` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `LinearMap.instFunLike` `TensorAlgebra.ι` `DirectSum.instModule` `DirectSum.lof` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `FreeTensorAlgebra`	—	—
`ι_apply` 📖	mathematical	—	`FreeTensorAlgebra` `instSemiringTensorAlgebra` `DirectSum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instAddCommMonoidDirectSum` `instModuleDirectSum` `rel` `RingQuot.Rel` `DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `TensorAlgebra` `Algebra.toModule` `instAlgebra` `Algebra.id` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `LinearMap.instFunLike` `TensorAlgebra.ι` `LinearAlgebra.FreeProduct` `RingQuot.instAddCommMonoid` `instSemiring` `instAlgebra` `ι'`	—	`IsScalarTower.left` `RingQuot.mkRingHom_def` `LinearMap.comp.congr_simp` `DirectSum.instIsScalarTower` `RingQuot.mkAlgHom_def`
`ι_def` 📖	mathematical	—	`ι` `AlgHom.ofLinearMap` `LinearAlgebra.FreeProduct` `instSemiring` `instAlgebra` `LinearMap.comp` `DirectSum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instAddCommMonoidDirectSum` `Algebra.toModule` `instModuleDirectSum` `RingHom.id` `ι'` `DirectSum.lof` `lof_map_one`	—	`lof_map_one`

RingQuot

Definitions

Name	Category	Theorems
`algEquivQuotAlgEquiv` 📖	CompOp	—
`equivQuotEquiv` 📖	CompOp	—

---

← Back to Index