Commit 2023-07-29 10:38 91917cb8
View on Github →feat: Data/Int/ModEq add theorem modEq_sub_fac, compliment modEq_add_fac (#6040) Easy of use function to compliment modEq_add_fac, the statement that : a = b [ZMOD n] implies a - c * n = b [ZMOD n]
feat: Data/Int/ModEq add theorem modEq_sub_fac, compliment modEq_add_fac (#6040) Easy of use function to compliment modEq_add_fac, the statement that : a = b [ZMOD n] implies a - c * n = b [ZMOD n]