Commit 2023-01-13 18:56 930a6c11

View on Github →

feat: port Algebra.Order.Pointwise (#1533)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Order/Pointwise.lean

added theorem LinearOrderedField.smul_Icc

added theorem LinearOrderedField.smul_Ici

added theorem LinearOrderedField.smul_Ico

added theorem LinearOrderedField.smul_Iic

added theorem LinearOrderedField.smul_Iio

added theorem LinearOrderedField.smul_Ioc

added theorem LinearOrderedField.smul_Ioi

added theorem LinearOrderedField.smul_Ioo

added theorem cinfₛ_div

added theorem cinfₛ_inv

added theorem cinfₛ_mul

added theorem cinfₛ_one

added theorem csupₛ_div

added theorem csupₛ_inv

added theorem csupₛ_mul

added theorem csupₛ_one

added theorem infₛ_div

added theorem infₛ_inv

added theorem infₛ_mul

added theorem infₛ_one

added theorem supₛ_div

added theorem supₛ_inv

added theorem supₛ_mul

added theorem supₛ_one