Some structure fields appear with unknown variable names in

[alexjbest]

On https://leanprover-community.github.io/mathlib_docs/linear_algebra/bilinear_form.html#bilin_form the declarations have this random c appearing before the bilin in bilin_add_left i.e.

structure bilin_form (R : Type u) (M : Type v) [ring R] [add_comm_group M] [module R M] :
Type (max u v)
(bilin : M → M → R)
(bilin_add_left : ∀ (x y z : M), c.bilin (x + y) z = c.bilin x z + c.bilin y z)
(bilin_smul_left : ∀ (a : R) (x y : M), c.bilin (a • x) y = a * c.bilin x y)
(bilin_add_right : ∀ (x y z : M), c.bilin x (y + z) = c.bilin x y + c.bilin x z)
(bilin_smul_right : ∀ (a : R) (x y : M), c.bilin x (a • y) = a * c.bilin x y)

the actual definition in lean is

bilin_form.bilin_add_left : ∀ {R : Type u} {M : Type v} [_inst_1 : ring R] [_inst_2 : add_comm_group M] [_inst_3 : module R M]
(c : bilin_form R M) (x y z : M), c.bilin (x + y) z = c.bilin x z + c.bilin y z b

so the c is an explicit argument in the generated equation.

Should doc-gen conform to the source code and not have c. or the output of #print and include (c : bilin_form R M). Leaving it as is seems like it could get confusing to me.