Commit 2022-11-29 20:56 0ef0e730

View on Github →

chore(Algebra/Order/Ring/Lemmas): fix names (#781)

Estimated changes

Modified Mathlib/Algebra/Order/Ring/Lemmas.lean

added theorem MulPosMono.toMulPosReflectLT

deleted theorem MulPosMono.to_mul_pos_reflect_lt

added theorem MulPosMonoRev.toMulPosStrictMono

deleted theorem MulPosMonoRev.to_mul_pos_strict_mono

added theorem MulPosReflectLT.toMulPosMono

deleted theorem MulPosReflectLT.to_mul_pos_mono

added theorem PosMulMono.toPosMulReflectLT

deleted theorem PosMulMono.to_pos_mul_reflect_lt

added theorem PosMulMonoRev.toPosMulStrictMono

deleted theorem PosMulMonoRev.to_pos_mul_strict_mono

added theorem PosMulReflectLT.toPosMulMono

deleted theorem PosMulReflectLT.to_pos_mul_mono

added theorem mulPosMono_iff_mulPosReflectLT

added theorem mulPosStrictMono_iff_mulPosMonoRev

deleted theorem mul_pos_mono_iff_mul_pos_reflect_lt

deleted theorem mul_pos_strict_mono_iff_mul_pos_mono_rev

added theorem posMulMono_iff_posMulReflectLT

added theorem posMulStrictMono_iff_posMulMonoRev

deleted theorem pos_mul_mono_iff_pos_mul_reflect_lt

deleted theorem pos_mul_strict_mono_iff_pos_mul_mono_rev