Commit 2024-09-10 17:17 0a23df42

View on Github →

feat (RingTheory/Valuation): add class IsValExtension (#14342) Add typeclass IsValExtension and related lemmas.

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/Valuation/ValExtension.lean

added theorem IsValExtension.algebraMap_injective

added theorem IsValExtension.ofComapInteger

added theorem IsValExtension.val_algebraMap

added theorem IsValExtension.val_map_eq_iff

added theorem IsValExtension.val_map_eq_one_iff

added theorem IsValExtension.val_map_le_iff

added theorem IsValExtension.val_map_le_one_iff

added theorem IsValExtension.val_map_lt_iff

added theorem IsValExtension.val_map_lt_one_iff

added theorem IsValExtension.val_smul