Mathlib Changelog
v4
Changelog
About
Github
Theorem
prod_mem_ideal_map_of_mem_conductor
Modification history
2025-09-03 11:07
Mathlib/NumberTheory/KummerDedekind.lean
chore(RingTheory/Conductor): move definition and results about the conductor ideal to a separate file (#29173) …
Modified
prod_mem_ideal_map_of_mem_conductor
View on Github →
2023-06-19 15:02
Mathlib/NumberTheory/KummerDedekind.lean
feat: port NumberTheory.KummerDedekind (#5249)
Added
prod_mem_ideal_map_of_mem_conductor
View on Github →