Commit 2023-06-08 18:50 ce3d1797

View on Github →

feat: port Algebra.Order.CompleteField (#4859) A statement in Analysis.SpecialFunctions.Pow.Real.lean was incorrect compared to the Mathlib3 version. I fixed it since it is used in this file.

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Order/CompleteField.lean

added theorem LinearOrderedField.coe_inducedOrderRingIso

added theorem LinearOrderedField.coe_lt_inducedMap_iff

added theorem LinearOrderedField.coe_mem_cutMap_iff

added def LinearOrderedField.cutMap

added theorem LinearOrderedField.cutMap_add

added theorem LinearOrderedField.cutMap_bddAbove

added theorem LinearOrderedField.cutMap_coe

added theorem LinearOrderedField.cutMap_mono

added theorem LinearOrderedField.cutMap_nonempty

added theorem LinearOrderedField.cutMap_self

added theorem LinearOrderedField.exists_mem_cutMap_mul_self_of_lt_inducedMap_mul_self

added def LinearOrderedField.inducedAddHom

added def LinearOrderedField.inducedMap

added theorem LinearOrderedField.inducedMap_add

added theorem LinearOrderedField.inducedMap_inducedMap

added theorem LinearOrderedField.inducedMap_inv_self

added theorem LinearOrderedField.inducedMap_mono

added theorem LinearOrderedField.inducedMap_nonneg

added theorem LinearOrderedField.inducedMap_one

added theorem LinearOrderedField.inducedMap_rat

added theorem LinearOrderedField.inducedMap_self

added theorem LinearOrderedField.inducedMap_zero

added def LinearOrderedField.inducedOrderRingHom

added def LinearOrderedField.inducedOrderRingIso

added theorem LinearOrderedField.inducedOrderRingIso_self

added theorem LinearOrderedField.inducedOrderRingIso_symm

added theorem LinearOrderedField.le_inducedMap_mul_self_of_mem_cutMap

added theorem LinearOrderedField.lt_inducedMap_iff

added theorem LinearOrderedField.mem_cutMap_iff

added theorem ringHom_monotone

Modified Mathlib/Analysis/SpecialFunctions/Pow/Real.lean