Documentation Verification Report

Defs

📁 Source: Mathlib/RingTheory/Ideal/Defs.lean

Statistics

Metric	Count
Definitions `IsTwoSided`, `inertia`, `eqIdeal`	3
Theorems `mul_mem_of_left`, `add_mem`, `add_mem_iff_left`, `add_mem_iff_right`, `ext`, `ext_iff`, `instIsTwoSided`, `instIsTwoSided_1`, `isTwoSided_iff`, `mem_of_dvd`, `mul_mem_left`, `mul_mem_right`, `mul_sub_mul_mem`, `mul_unit_mem_iff_mem`, `neg_mem_iff`, `pow_mem_of_mem`, `pow_mem_of_pow_mem`, `sub_mem`, `unit_mul_mem_iff_mem`, `zero_mem`	20
Total	23

Ideal

Definitions

Name	Category	Theorems
`IsTwoSided` 📖	CompData	19 math math: `instCanLiftTwoSidedIdealCoeOrderHomAsIdealIsTwoSided`, `TwoSidedIdeal.instIsTwoSidedCoeOrderHomIdealAsIdeal`, `instIsTwoSidedJacobson`, `Submodule.instIsTwoSidedColonCoe`, `TwoSidedIdeal.orderIsoIsTwoSided_symm_apply`, `isTwoSided_iff`, `instIsTwoSidedBot`, `instIsTwoSided`, `RingHom.instIsTwoSidedKer`, `instIsTwoSidedAnnihilator`, `IsTwoSided.instHPowNat`, `instIsTwoSided_1`, `instIsTwoSidedTop`, `Ring.instIsTwoSidedJacobson`, `instIsTwoSidedMapRingHomOfRingHomSurjective`, `isFullyInvariant_iff_isTwoSided`, `TwoSidedIdeal.orderIsoIsTwoSided_apply_coe`, `IsTwoSided.instHMul`, `instIsTwoSidedComap`
`inertia` 📖	CompOp	9 math math: `Quotient.map_ker_stabilizer_subtype`, `IsArithFrobAt.mul_inv_mem_inertia`, `inertia_le_stabilizer`, `Quotient.stabilizerQuotientInertiaEquiv_mk`, `card_inertia_eq_ramificationIdxIn`, `Quotient.ker_stabilizerHom`, `card_stabilizer_eq_card_inertia_mul_finrank`, `ncard_primesOver_mul_card_inertia_mul_finrank`, `instNormalSubtypeMemSubgroupStabilizerSubgroupOfInertia`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add_mem` 📖	mathematical	`Ideal` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	`Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib`	—	`Submodule.add_mem`
`add_mem_iff_left` 📖	mathematical	`Ideal` `Ring.toSemiring` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	`Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	—	`Submodule.add_mem_iff_left`
`add_mem_iff_right` 📖	mathematical	`Ideal` `Ring.toSemiring` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	`Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	—	`Submodule.add_mem_iff_right`
`ext` 📖	—	`Ideal` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	—	—	`Submodule.ext`
`ext_iff` 📖	mathematical	—	`Ideal` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	—	`ext`
`instIsTwoSided` 📖	mathematical	—	`IsTwoSided` `CommSemiring.toSemiring`	—	`Submodule.smul_mem` `mul_comm`
`instIsTwoSided_1` 📖	mathematical	—	`IsTwoSided` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	—	`instIsTwoSided`
`isTwoSided_iff` 📖	mathematical	—	`IsTwoSided` `Ideal` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	—
`mem_of_dvd` 📖	—	`semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `NonUnitalCommSemiring.toNonUnitalSemiring` `CommSemiring.toNonUnitalCommSemiring` `Ideal` `CommSemiring.toSemiring` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	—	—	`mul_mem_right` `instIsTwoSided`
`mul_mem_left` 📖	mathematical	`Ideal` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`Submodule.smul_mem`
`mul_mem_right` 📖	mathematical	`Ideal` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`IsTwoSided.mul_mem_of_left`
`mul_sub_mul_mem` 📖	mathematical	`Ideal` `Ring.toSemiring` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne`	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	—	`sub_mul` `mul_sub` `Mathlib.Tactic.Abel.unfold_sub` `Mathlib.Tactic.Abel.subst_into_addg` `Mathlib.Tactic.Abel.term_atomg` `Mathlib.Tactic.Abel.subst_into_negg` `Mathlib.Tactic.Abel.term_neg` `neg_zero` `Mathlib.Tactic.Abel.term_add_constg` `zero_add` `Mathlib.Tactic.Abel.const_add_termg` `add_zero` `Mathlib.Tactic.Abel.term_add_termg` `Mathlib.Meta.NormNum.IsNat.to_eq` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Meta.NormNum.isInt_neg` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Tactic.Abel.zero_termg` `add_mem` `mul_mem_right` `mul_mem_left`
`mul_unit_mem_iff_mem` 📖	mathematical	`IsUnit` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring`	`Ideal` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`unit_mul_mem_iff_mem` `mul_comm`
`neg_mem_iff` 📖	mathematical	—	`Ideal` `Ring.toSemiring` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup`	—	`Submodule.neg_mem_iff`
`pow_mem_of_mem` 📖	mathematical	`Ideal` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	`Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	—	`mul_mem_left` `pow_succ`
`pow_mem_of_pow_mem` 📖	—	`Ideal` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	—	—	`add_comm` `pow_add` `mul_mem_left`
`sub_mem` 📖	mathematical	`Ideal` `Ring.toSemiring` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	`SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne`	—	`Submodule.sub_mem`
`unit_mul_mem_iff_mem` 📖	mathematical	`IsUnit` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	`Ideal` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`IsUnit.exists_left_inv` `mul_mem_left` `one_mul` `mul_assoc`
`zero_mem` 📖	mathematical	—	`Ideal` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`Submodule.zero_mem`

Ideal.IsTwoSided

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mul_mem_of_left` 📖	mathematical	`Ideal` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	—

Module

Definitions

Name	Category	Theorems
`eqIdeal` 📖	CompOp	—

---

← Back to Index