Mathlib v3 is deprecated. Go to Mathlib v4

Theorem subfield.is_closed_topological_closure

Modification history

2022-12-07 18:26
src/topology/algebra/field.lean
feat(topology/algebra/uniform_ring): add dense_inducing.extend_hom (#17212) …
Added subfield.is_closed_topological_closureView on Github →