Documentation Verification Report

Basic

📁 Source: Mathlib/RingTheory/Ideal/Quotient/Basic.lean

Statistics

Metric	Count
Definitions `divisionRing`, `groupWithZero`, `instUniqueQuotientTop`, `modulePi`, `piQuotEquiv`	5
Theorems `of_finite_quot_finite_ideal`, `of_ideal_quotient`, `eq_zero_iff_dvd`, `exists_inv`, `isDomain`, `isDomain_iff_prime`, `isScalarTower_right`, `maximal_ideal_iff_isField_quotient`, `maximal_of_isField`, `mk_singleton_self`, `mk_span_range`, `noZeroDivisors`, `nontrivial`, `nontrivial_iff`, `smulCommClass`, `smulCommClass'`, `subsingleton_iff`, `zero_eq_one_iff`, `zero_ne_one_iff`, `map_pi`, `univ_eq_iUnion_image_add`, `finite_iff_ideal_quotient`	22
Total	27

Finite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`of_finite_quot_finite_ideal` 📖	mathematical	—	`Finite`	—	`of_ideal_quotient`
`of_ideal_quotient` 📖	mathematical	—	`Finite`	—	`finite_iff_ideal_quotient`

Ideal

Definitions

Name	Category	Theorems
`modulePi` 📖	CompOp	—
`piQuotEquiv` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`map_pi` 📖	mathematical	`Ideal` `Ring.toSemiring` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	`DFunLike.coe` `LinearMap` `RingHom.id` `Pi.addCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Pi.Function.module` `LinearMap.instFunLike`	—	`nonempty_fintype` `pi_eq_sum_univ` `map_sum` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `Finset.sum_congr` `map_smul` `SemilinearMapClass.toMulActionSemiHomClass` `Finset.sum_apply` `Submodule.sum_mem` `mul_mem_right`
`univ_eq_iUnion_image_add` 📖	mathematical	—	`Set.univ` `Set.iUnion` `HasQuotient.Quotient` `Ideal` `Ring.toSemiring` `instHasQuotient` `HVAdd.hVAdd` `Set` `instHVAdd` `Set.vaddSet` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `AddMonoidWithOne.toAddMonoid` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `AddAction.toAddSemigroupAction` `AddMonoid.toAddAction` `Quotient.out` `Submodule.quotientRel` `Ring.toAddCommGroup` `Semiring.toModule` `SetLike.coe` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`QuotientAddGroup.univ_eq_iUnion_vadd`

Ideal.Quotient

Definitions

Name	Category	Theorems
`divisionRing` 📖	CompOp	—
`groupWithZero` 📖	CompOp	—
`instUniqueQuotientTop` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_zero_iff_dvd` 📖	mathematical	—	`DFunLike.coe` `RingHom` `HasQuotient.Quotient` `Ideal` `Ring.toSemiring` `CommRing.toRing` `Ideal.instHasQuotient` `Ideal.span` `Set` `Set.instSingletonSet` `Semiring.toNonAssocSemiring` `ring` `Ideal.instIsTwoSided_1` `RingHom.instFunLike` `Submodule.Quotient.instZeroQuotient` `Ring.toAddCommGroup` `Semiring.toModule` `semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `NonUnitalCommSemiring.toNonUnitalSemiring` `NonUnitalCommRing.toNonUnitalCommSemiring` `CommRing.toNonUnitalCommRing`	—	`Ideal.instIsTwoSided_1` `eq_zero_iff_mem` `Ideal.mem_span_singleton`
`exists_inv` 📖	mathematical	—	`HasQuotient.Quotient` `Ideal` `Ring.toSemiring` `Ideal.instHasQuotient` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `ring` `one`	—	`exists_right_inv_of_exists_left_inv` `Ideal.IsMaximal.exists_inv` `eq_zero_iff_mem` `neg_sub` `neg_mem_iff` `AddSubgroupClass.toNegMemClass` `Submodule.addSubgroupClass` `eq_sub_iff_add_eq'`
`isDomain` 📖	mathematical	—	`IsDomain` `HasQuotient.Quotient` `Ideal` `Ring.toSemiring` `Ideal.instHasQuotient` `ring`	—	`nontrivial_iff` `Ideal.IsPrime.ne_top'` `NoZeroDivisors.to_isDomain` `noZeroDivisors`
`isDomain_iff_prime` 📖	mathematical	—	`IsDomain` `HasQuotient.Quotient` `Ideal` `Ring.toSemiring` `Ideal.instHasQuotient` `ring` `Ideal.IsPrime`	—	`zero_ne_one_iff` `zero_ne_one` `NeZero.one` `Nontrivial.exists_pair_ne` `IsDomain.toNontrivial` `NoZeroDivisors.eq_zero_or_eq_zero_of_mul_eq_zero` `IsDomain.to_noZeroDivisors` `RingHom.map_mul` `isDomain`
`isScalarTower_right` 📖	mathematical	—	`IsScalarTower` `HasQuotient.Quotient` `Ideal` `Ring.toSemiring` `Ideal.instHasQuotient` `Submodule.Quotient.instSMul'` `Ring.toAddCommGroup` `Semiring.toModule` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `ring` `DistribSMul.toSMulZeroClass` `instDistribSMul` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	—	`RingCon.isScalarTower_right`
`maximal_ideal_iff_isField_quotient` 📖	mathematical	—	`Ideal.IsMaximal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `IsField` `HasQuotient.Quotient` `Ideal` `Ideal.instHasQuotient_1` `semiring`	—	`Field.toIsField` `maximal_of_isField`
`maximal_of_isField` 📖	mathematical	`IsField` `HasQuotient.Quotient` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Ideal.instHasQuotient_1` `semiring`	`Ideal.IsMaximal`	—	`Ideal.isMaximal_iff` `IsField.exists_pair_ne` `Ideal.instIsTwoSided_1` `eq` `Ideal.mul_mem_left` `mul_one` `IsField.mul_inv_cancel` `eq_zero_iff_mem` `zero_add` `sub_self` `sub_add` `Ideal.sub_mem` `Ideal.mul_mem_right`
`mk_singleton_self` 📖	mathematical	—	`DFunLike.coe` `RingHom` `HasQuotient.Quotient` `Ideal` `Ring.toSemiring` `Ideal.instHasQuotient` `Ideal.span` `Set` `Set.instSingletonSet` `Semiring.toNonAssocSemiring` `ring` `RingHom.instFunLike` `Submodule.Quotient.instZeroQuotient` `Ring.toAddCommGroup` `Semiring.toModule`	—	`Submodule.Quotient.mk_eq_zero` `Ideal.mem_span_singleton_self`
`mk_span_range` 📖	mathematical	—	`DFunLike.coe` `RingHom` `HasQuotient.Quotient` `Ideal` `Ring.toSemiring` `Ideal.instHasQuotient` `Ideal.span` `Set.range` `Semiring.toNonAssocSemiring` `ring` `RingHom.instFunLike` `Submodule.Quotient.instZeroQuotient` `Ring.toAddCommGroup` `Semiring.toModule`	—	`eq_zero_iff_mem` `Ideal.subset_span`
`noZeroDivisors` 📖	mathematical	—	`NoZeroDivisors` `HasQuotient.Quotient` `Ideal` `Ring.toSemiring` `Ideal.instHasQuotient` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `ring` `Submodule.Quotient.instZeroQuotient` `Ring.toAddCommGroup` `Semiring.toModule`	—	`Quotient.inductionOn₂'` `Ideal.IsPrime.mem_or_mem` `eq_zero_iff_mem`
`nontrivial` 📖	mathematical	—	`Nontrivial` `HasQuotient.Quotient` `Ideal` `Ring.toSemiring` `Ideal.instHasQuotient`	—	`nontrivial_iff`
`nontrivial_iff` 📖	mathematical	—	`Nontrivial` `HasQuotient.Quotient` `Ideal` `Ring.toSemiring` `Ideal.instHasQuotient`	—	`Submodule.Quotient.nontrivial_iff`
`smulCommClass` 📖	mathematical	—	`SMulCommClass` `HasQuotient.Quotient` `Ideal` `Ring.toSemiring` `Ideal.instHasQuotient` `Submodule.Quotient.instSMul'` `Ring.toAddCommGroup` `Semiring.toModule` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `ring` `DistribSMul.toSMulZeroClass` `instDistribSMul` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	—	`RingCon.smulCommClass`
`smulCommClass'` 📖	mathematical	—	`SMulCommClass` `HasQuotient.Quotient` `Ideal` `Ring.toSemiring` `Ideal.instHasQuotient` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `ring` `DistribSMul.toSMulZeroClass` `instDistribSMul` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Submodule.Quotient.instSMul'` `Ring.toAddCommGroup` `Semiring.toModule`	—	`RingCon.smulCommClass'`
`subsingleton_iff` 📖	mathematical	—	`HasQuotient.Quotient` `Ideal` `Ring.toSemiring` `Ideal.instHasQuotient` `Top.top` `Submodule.instTop` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	—	`Submodule.Quotient.subsingleton_iff`
`zero_eq_one_iff` 📖	mathematical	—	`HasQuotient.Quotient` `Ideal` `Ring.toSemiring` `Ideal.instHasQuotient` `Submodule.Quotient.instZeroQuotient` `Ring.toAddCommGroup` `Semiring.toModule` `one` `Top.top` `Submodule.instTop` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`Submodule.Quotient.mk_eq_zero` `Ideal.eq_top_iff_one`
`zero_ne_one_iff` 📖	—	—	—	—	`zero_eq_one_iff`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`finite_iff_ideal_quotient` 📖	mathematical	—	`Finite` `Ideal` `Ring.toSemiring` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `HasQuotient.Quotient` `Ideal.instHasQuotient`	—	`finite_iff_addSubgroup_quotient`

---

← Back to Index