Theorems · Theorem · commutative algebra

Algebra.IsInvariant.orbit_eq_primesOver

∀ (A : Type u_1) (B : Type u_2) (G : Type u_3) [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B]
  [inst_3 : Group G] [inst_4 : MulSemiringAction G B] [Algebra.IsInvariant A B G] [Finite G] [SMulCommClass G A B]
  (P : Ideal A) (Q : Ideal B) [hP : Q.LiesOver P] [hQ : Q.IsPrime], MulAction.orbit G Q = P.primesOver B

Defined in: Mathlib.RingTheory.Invariant.Basic
Cited by: 2 results in Mathlib
Foundations: Depth 99 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: CommRing CommRing Algebra Group MulSemiringAction Algebra.IsInvariant Finite SMulCommClass Ideal.LiesOver Ideal.IsPrime

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites17

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Setstatement · cited by 53,352
CommRingstatement and proof · cited by 17,173
Algebrastatement and proof · cited by 11,388
Groupstatement and proof · cited by 6,238
Idealstatement and proof · cited by 4,748
Finitestatement and proof · cited by 3,029
Set.extproof · cited by 2,266
SMulCommClassstatement and proof · cited by 1,927
Ideal.IsPrimestatement and proof · cited by 827
MulSemiringActionstatement and proof · cited by 423
Ideal.LiesOverstatement and proof · cited by 272
MulAction.orbitstatement and proof · cited by 114

Cited by2

Results whose statement or proof uses this declaration.

Ideal.ncard_primesOver_mul_card_inertia_mul_finrankproof · cited by 1
Ideal.ncard_primesOver_mul_ncard_primesOverproof · cited by 0