Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-01 20:54 5c2fa35a

View on Github →

chore(topology/algebra/valuation): add universe (#11962)

Estimated changes

modified theorem valued.loc_const
modified theorem valued.subgroups_basis
modified theorem valued.continuous_extension
modified theorem valued.continuous_valuation
modified theorem valued.extension_extends