Duplication

Stream: mathlib4

[Sébastien Gouëzel]

I have just noticed that we have docs#innerₛₗ and docs#sesqFormOfInner, which are almost identical. Does an expert on this area of Mathlib know whether this is deliberate?

[Eric Wieser]

docs3#innerₛₗ, docs3#sesq_form_of_inner suggests that both have been around for a long time

[Ruben Van de Velde]

The latter used to be a sesq_form before mathlib3#10443

[Moritz Doll]

Yeah, it seems to be like a artifact from when we had sesq_form. Probably get rid of docs#sesqFormOfInner and see how much it breaks (shouldn't be too bad)

[Sébastien Gouëzel]

Done in #33316