Theorems · Definition · commutative algebra
Ideal.inertia
{α : Type u} → [inst : Ring α] → (G : Type u_1) → [inst_1 : Group G] → [MulAction G α] → Ideal α → Subgroup GThe subgroup of elements g of G such that ∀ x, g • x - x ∈ I.
- Defined in
- Mathlib.RingTheory.Ideal.Defs
- Cited by
- 21 results in Mathlib
- Foundations
- Depth 20 from the axioms · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites7
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Ringstatement and proof · cited by 7,463
- Groupstatement and proof · cited by 6,238
- Idealstatement and proof · cited by 4,748
- Subgroupstatement · cited by 3,593
- MulActionstatement and proof · cited by 1,294
- Submodule.toAddSubgroupproof · cited by 106
- AddSubgroup.inertiaproof · cited by 6
Cited by27
Results whose statement or proof uses this declaration.
- Ideal.inertiaEquivstatement and proof · cited by 4
- IsInertiaField.ringEquivproof · cited by 2
- Ideal.card_inertia_eq_ramificationIdxInstatement and proof · cited by 2
- Ideal.card_stabilizer_eq_card_inertia_mul_finrankstatement and proof · cited by 2
- Ideal.Quotient.ker_stabilizerHomstatement · cited by 2
- IsFractionRing.stabilizerQuotientInertiaEquivstatement and proof · cited by 2
- IsInertiaField.casesOnstatement and proof · cited by 1
- IsInertiaField.rank_leftproof · cited by 1
- Ideal.inertiaEquiv_apply_smulstatement and proof · cited by 1
- Ideal.Quotient.stabilizerQuotientInertiaEquivstatement and proof · cited by 1
- Ideal.inertiaEquiv_symm_apply_smulstatement and proof · cited by 1
- Ideal.inertia_le_stabilizerstatement and proof · cited by 1