Theorem IsIntegrallyClosed.exists_algebraMap_eq_of_pow_mem_subalgebra

Modification history

2023-09-19 10:04
Mathlib/RingTheory/IntegrallyClosed.lean
feat: `IsDedekindRing` is `IsDedekindDomain` minus `IsDomain` (#6127) …
Modified IsIntegrallyClosed.exists_algebraMap_eq_of_pow_mem_subalgebraView on Github →
2023-08-10 19:52
Mathlib/RingTheory/IntegrallyClosed.lean
chore: banish `Type _` and `Sort _` (#6499) …
Modified IsIntegrallyClosed.exists_algebraMap_eq_of_pow_mem_subalgebraView on Github →
2023-06-02 10:22
Mathlib/RingTheory/IntegrallyClosed.lean
feat: port RingTheory.IntegrallyClosed (#4574)
Added IsIntegrallyClosed.exists_algebraMap_eq_of_pow_mem_subalgebraView on Github →