Commit 2025-05-05 14:19 4fefe1cb

View on Github →

chore(RingTheory/Valuation/Extension): rename IsValExtension to Valuation.HasExtension (#23584) This change is to remove IsValExtension from the root namespace and to allow dot notation.

Estimated changes

Modified Mathlib.lean

Renamed Mathlib/RingTheory/Valuation/ValExtension.lean to Mathlib/RingTheory/Valuation/Extension.lean

deleted theorem IsValExtension.algebraMap_injective

deleted theorem IsValExtension.instIsLocalHomValuationInteger

deleted theorem IsValExtension.ofComapInteger

deleted theorem IsValExtension.val_algebraMap

deleted theorem IsValExtension.val_map_eq_iff

deleted theorem IsValExtension.val_map_eq_one_iff

deleted theorem IsValExtension.val_map_le_iff

deleted theorem IsValExtension.val_map_le_one_iff

deleted theorem IsValExtension.val_map_lt_iff

deleted theorem IsValExtension.val_map_lt_one_iff

deleted theorem IsValExtension.val_smul

added theorem Valuation.HasExtension.algebraMap_injective

added theorem Valuation.HasExtension.instIsLocalHomValuationInteger

added theorem Valuation.HasExtension.ofComapInteger

added theorem Valuation.HasExtension.val_algebraMap

added theorem Valuation.HasExtension.val_map_eq_iff

added theorem Valuation.HasExtension.val_map_eq_one_iff

added theorem Valuation.HasExtension.val_map_le_iff

added theorem Valuation.HasExtension.val_map_le_one_iff

added theorem Valuation.HasExtension.val_map_lt_iff

added theorem Valuation.HasExtension.val_map_lt_one_iff

added theorem Valuation.HasExtension.val_smul