Theorem Ideal.under_smul

Modification history

2025-06-17 04:38

Mathlib/RingTheory/Ideal/Over.lean

refactor(NumberTheory/RamificationInertia/Galois): Generalize action on `primesOver` to arbitrary group (#25995) …

Modified Ideal.under_smul View on Github →

2024-10-28 23:09

Mathlib/RingTheory/Ideal/Over.lean

refactor(RingTheory/Ideal/Pointwise): Generalize to semirings (#18355) …

Added Ideal.under_smul View on Github →