Commit 2023-03-19 08:24 c78cad35

View on Github →

chore(analysis/inner_product_space/basic): explicit 𝕜 argument for innerₛₗ and innerSL (#18613) A reasonable fraction of the uses of these functions required either @ or a type annotation before this change.

Estimated changes

Modified src/analysis/convex/cone/basic.lean

Modified src/analysis/inner_product_space/basic.lean

modified theorem innerSL_apply

modified theorem innerSL_apply_coe

modified theorem innerSL_apply_norm

modified theorem innerSL_flip_apply

modified theorem innerₛₗ_apply

modified theorem innerₛₗ_apply_coe

modified theorem orthogonal_eq_inter

Modified src/analysis/inner_product_space/calculus.lean

Modified src/analysis/inner_product_space/dual.lean

modified theorem inner_product_space.innerSL_norm

Modified src/analysis/inner_product_space/l2_space.lean

Modified src/analysis/inner_product_space/pi_L2.lean

Modified src/analysis/inner_product_space/rayleigh.lean

Modified src/analysis/inner_product_space/two_dim.lean

Modified src/geometry/manifold/instances/sphere.lean

Modified src/measure_theory/integral/set_integral.lean