Zulip Chat Archive
Stream: new members
Topic: vector
Alex Zhang (Jul 05 2021 at 03:43):
Are the vector of one's and related simplification lemmas defined in mathlib?
Alex Zhang (Jul 05 2021 at 05:05):
I suspect no. I am wrting some.
Kevin Buzzard (Jul 05 2021 at 07:34):
docs#vector.repeat (guessing)
Eric Wieser (Jul 05 2021 at 07:45):
docs#pi.has_one means (1 : fin n → ℝ) works as you'd expect
Last updated: Dec 20 2023 at 11:08 UTC