Mathlib v3 is deprecated. Go to Mathlib v4

Theorem prod_mem_ideal_map_of_mem_conductor

Modification history

2022-10-19 07:41

src/number_theory/kummer_dedekind.lean

feat(number_theory/kummer_dedekind): define conductor and add basic API plus theorem (#16833) …

Added prod_mem_ideal_map_of_mem_conductor View on Github →