mathlib3
90bc9579 - chore(analysis/inner_product_space): move `is_symmetric` to a new file lower in the import tree (#16106)

Commit
3 years ago
chore(analysis/inner_product_space): move `is_symmetric` to a new file lower in the import tree (#16106)
Author
Parents
Loading