Commit 2025-11-18 16:33 fd6ea04d

View on Github →

feat: characterise regular elements of type synonyms (#31739)

Estimated changes

added theorem isAddLeftRegular_ofMul
added theorem isAddLeftRegular_toAdd
added theorem isAddRegular_ofMul
added theorem isAddRegular_toAdd
added theorem isLeftRegular_ofAdd
added theorem isLeftRegular_toMul
added theorem isRegular_ofAdd
added theorem isRegular_toMul
added theorem isRightRegular_ofAdd
added theorem isRightRegular_toMul
added theorem isLeftRegular_ofColex
added theorem isLeftRegular_ofDual
added theorem isLeftRegular_ofLex
added theorem isLeftRegular_toColex
added theorem isLeftRegular_toDual
added theorem isLeftRegular_toLex
added theorem isRegular_ofColex
added theorem isRegular_ofDual
added theorem isRegular_ofLex
added theorem isRegular_toColex
added theorem isRegular_toDual
added theorem isRegular_toLex
added theorem isRightRegular_ofColex
added theorem isRightRegular_ofDual
added theorem isRightRegular_ofLex
added theorem isRightRegular_toColex
added theorem isRightRegular_toDual
added theorem isRightRegular_toLex
added theorem ofDual_eq_one
added theorem toDual_eq_one
added theorem Additive.ofMul_bot
added theorem Additive.ofMul_eq_bot
added theorem Additive.ofMul_eq_top
added theorem Additive.ofMul_top
added theorem Additive.toMul_bot
added theorem Additive.toMul_eq_bot
added theorem Additive.toMul_eq_top
added theorem Additive.toMul_top
modified theorem OrderDual.ofDual_bot
modified theorem OrderDual.ofDual_top
modified theorem OrderDual.toDual_bot
modified theorem OrderDual.toDual_top