Skip to content

feat(NumberTheory/RamificationInertia/Unramified): generalize IsUnramifiedAt.of_liesOver to flat algebras - #42919

Open
tb65536 wants to merge 3 commits into
leanprover-community:masterfrom
tb65536:tb_ramidx93
Open

feat(NumberTheory/RamificationInertia/Unramified): generalize IsUnramifiedAt.of_liesOver to flat algebras#42919
tb65536 wants to merge 3 commits into
leanprover-community:masterfrom
tb65536:tb_ramidx93