Commit 2022-11-20 20:44 7a3282ce

View on Github →

feat: port Algebra.Group.OrderSynonym (#651) Tracking mathlib commit: c3019c79074b0619edb4b27553a91b2e82242395

Estimated changes

added theorem ofDual_div
added theorem ofDual_inv
added theorem ofDual_mul
added theorem ofDual_one
added theorem ofDual_pow
added theorem ofDual_smul'
added theorem ofDual_smul
added theorem ofLex_div
added theorem ofLex_inv
added theorem ofLex_mul
added theorem ofLex_one
added theorem ofLex_pow
added theorem ofLex_smul'
added theorem ofLex_smul
added theorem pow_ofDual
added theorem pow_ofLex
added theorem pow_toDual
added theorem pow_toLex
added theorem toDual_div
added theorem toDual_inv
added theorem toDual_mul
added theorem toDual_one
added theorem toDual_pow
added theorem toDual_smul'
added theorem toDual_smul
added theorem toLex_div
added theorem toLex_inv
added theorem toLex_mul
added theorem toLex_one
added theorem toLex_pow
added theorem toLex_smul'
added theorem toLex_smul