Documentation Verification Report

Epi

📁 Source: Mathlib/Algebra/Algebra/Epi.lean

Statistics

Metric	Count
Definitions `IsEpi`, `lid'`	2
Theorems `injective_lift_mul`, `injective_lift_lsmul`, `instIsEpiOfIsDomainOfIsFractionRing`, `isEpi_iff_forall_one_tmul_eq`, `isEpi_iff_surjective_algebraMap_of_finite`, `isEpi_of_surjective_algebraMap`, `tmul_comm`, `surjective_of_tmul_eq_tmul_of_finite`, `lid'_apply_tmul`, `lid'_symm_apply`	10
Total	12

Algebra

Definitions

Name	Category	Theorems
`IsEpi` 📖	CompData	7 math math: `RingHom.surjective_of_tmul_eq_tmul_of_finite`, `isEpi_of_surjective_algebraMap`, `CommRingCat.epi_iff_tmul_eq_tmul`, `CommRingCat.epi_iff_epi`, `instIsEpiOfIsDomainOfIsFractionRing`, `isEpi_iff_surjective_algebraMap_of_finite`, `isEpi_iff_forall_one_tmul_eq`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`injective_lift_lsmul` 📖	mathematical	—	`TensorProduct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `toModule` `DFunLike.coe` `LinearMap` `RingHom.id` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `LinearMap.instFunLike` `TensorProduct.lift` `LinearMap.restrictScalars₁₂` `Semiring.toModule` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `toSMul` `IsScalarTower.right` `LinearMap.lsmul`	—	`smulCommClass_self` `add_smul` `TensorProduct.tmul_add` `smul_assoc` `TensorProduct.tmul_smul` `TensorProduct.CompatibleSMul.isScalarTower` `IsScalarTower.left` `LinearMap.ext` `TensorProduct.add_tmul` `one_smul` `tmul_comm` `RingHomCompTriple.ids` `IsScalarTower.right` `TensorProduct.AlgebraTensorModule.curry_injective` `TensorProduct.isScalarTower` `IsScalarTower.to_smulCommClass`
`instIsEpiOfIsDomainOfIsFractionRing` 📖	mathematical	—	`IsEpi` `CommRing.toCommSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield`	—	`isEpi_iff_forall_one_tmul_eq` `IsFractionRing.div_surjective` `IsFractionRing.instFaithfulSMul` `IsDomain.to_noZeroDivisors` `IsDomain.toNontrivial` `smul_div_assoc` `IsScalarTower.right` `algebraMap_eq_smul_one` `TensorProduct.smul_tmul` `TensorProduct.CompatibleSMul.isScalarTower` `IsScalarTower.left` `smul_def` `mul_div_cancel₀`
`isEpi_iff_forall_one_tmul_eq` 📖	mathematical	—	`IsEpi` `TensorProduct.tmul` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `toModule` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`IsEpi.injective_lift_mul` `to_smulCommClass` `IsScalarTower.right` `one_mul` `mul_one` `TensorProduct.induction_on` `TensorProduct.zero_tmul` `TensorProduct.add_tmul`
`isEpi_iff_surjective_algebraMap_of_finite` 📖	mathematical	—	`IsEpi` `CommRing.toCommSemiring` `Ring.toSemiring` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `RingHom.instFunLike` `algebraMap`	—	`RingHomSurjective.ids` `subsingleton_or_nontrivial` `LinearMap.range_eq_top` `Submodule.Quotient.subsingleton_iff` `TensorProduct.induction_on` `Submodule.mkQ_surjective` `to_smulCommClass` `IsScalarTower.right` `isEpi_iff_forall_one_tmul_eq` `mul_one` `one_mul` `Submodule.Quotient.mk_eq_zero` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `TensorProduct.map_tmul` `TensorProduct.zero_tmul` `zero_add` `false_of_nontrivial_of_subsingleton` `instNontrivialTensorProduct` `Module.Finite.quotient` `isEpi_of_surjective_algebraMap`
`isEpi_of_surjective_algebraMap` 📖	mathematical	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `RingHom.instFunLike` `algebraMap`	`IsEpi`	—	`isEpi_iff_forall_one_tmul_eq` `algebraMap_eq_smul_one` `TensorProduct.smul_tmul` `TensorProduct.CompatibleSMul.isScalarTower` `IsScalarTower.left`
`tmul_comm` 📖	mathematical	—	`TensorProduct.tmul` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `toModule`	—	`to_smulCommClass` `TensorProduct.tmul_eq_smul_one_tmul` `isEpi_iff_forall_one_tmul_eq` `SMulCommClass.smul_comm` `TensorProduct.smulCommClass_left`

Algebra.IsEpi

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`injective_lift_mul` 📖	mathematical	—	`TensorProduct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `LinearMap.instFunLike` `TensorProduct.lift` `LinearMap.mul` `Algebra.to_smulCommClass` `IsScalarTower.right`	—	—

RingHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`surjective_of_tmul_eq_tmul_of_finite` 📖	mathematical	—	`Algebra.IsEpi` `CommRing.toCommSemiring` `Ring.toSemiring` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instFunLike` `algebraMap`	—	`Algebra.isEpi_iff_surjective_algebraMap_of_finite`

TensorProduct

Definitions

Name	Category	Theorems
`lid'` 📖	CompOp	2 math math: `lid'_apply_tmul`, `lid'_symm_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`lid'_apply_tmul` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `TensorProduct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Algebra.toModule` `addCommMonoid` `leftModule` `Semiring.toModule` `Algebra.to_smulCommClass` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `lid'` `tmul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction`	—	`RingHomInvPair.ids` `Algebra.to_smulCommClass`
`lid'_symm_apply` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `TensorProduct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Algebra.toModule` `addCommMonoid` `leftModule` `Semiring.toModule` `Algebra.to_smulCommClass` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `LinearEquiv.symm` `lid'` `tmul` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`LinearEquiv.injective` `Algebra.to_smulCommClass` `RingHomInvPair.ids` `LinearEquiv.apply_symm_apply` `one_smul`

---

← Back to Index