diff options
| author | Kazuhiko Sakaguchi | 2020-10-10 18:49:29 +0900 |
|---|---|---|
| committer | Kazuhiko Sakaguchi | 2020-10-23 17:48:47 +0900 |
| commit | 06b3e9011984666dde6a74b7b7a08b470763bd67 (patch) | |
| tree | 81eaff982a7e597d42c904c5014c57d197dfd9ea /mathcomp/_CoqProject | |
| parent | 2b97a257956d307e7cb9ad7d4920fb5db969b69b (diff) | |
New iteration/bigop lemmas in ssralg
- Add `iter_addr`, `iter_mulr(_1)`, and `prodr_const_nat`.
- Export `iter_addr_0`, `sumr_const_nat`, and the above lemmas from
`GRing.Theory`.
Diffstat (limited to 'mathcomp/_CoqProject')
0 files changed, 0 insertions, 0 deletions