| changeset 64242 | 93c6f0da5c70 |
| parent 61694 | 6571c78c9667 |
| child 67406 | 23307fd33906 |
| 64241:430d74089d4d | 64242:93c6f0da5c70 |
|---|---|
84 |
84 |
85 text{* |
85 text{* |
86 @{thm[display] mod_if[no_vars]} |
86 @{thm[display] mod_if[no_vars]} |
87 \rulename{mod_if} |
87 \rulename{mod_if} |
88 |
88 |
89 @{thm[display] mod_div_equality[no_vars]} |
89 @{thm[display] div_mult_mod_eq[no_vars]} |
90 \rulename{mod_div_equality} |
90 \rulename{div_mult_mod_eq} |
91 |
91 |
92 |
92 |
93 @{thm[display] div_mult1_eq[no_vars]} |
93 @{thm[display] div_mult1_eq[no_vars]} |
94 \rulename{div_mult1_eq} |
94 \rulename{div_mult1_eq} |
95 |
95 |