Some open statements don't resolve names

leanprover-community / mathport

Mathport is a tool for porting Lean3 projects to Lean4

Apache License 2.0

43 stars 15 forks source link

Closed gebner closed 2 years ago

gebner commented 2 years ago

open continuous_linear_map (smulRight smul_right_one_eq_iff)

should be:

open ContinuousLinearMap (smulRight smul_right_one_eq_iff)