mathlib
f9f64f37 - move(data/prod/*): A `prod` folder (#13771)

Commit
3 years ago
move(data/prod/*): A `prod` folder (#13771) Create folder `data.prod.` to hold `prod` files and related types. Precisely: * `data.prod` → `data.prod.basic` * `data.pprod` → `data.prod.pprod` * `data.tprod` → `data.prod.tprod` * `order.lexicographic` → `data.prod.lex`
Author
Parents
Loading