Commit 2023-03-24 18:27 d11893b4

View on Github →

fix(*): missing universe polymorphism (#18644) These are all just typo fixes, no proof adaptations. This deliberately leaves alone things related to category theory and algebraic geometry, as there the lack of polymorphism is likely deliberate.

Estimated changes

Modified src/analysis/normed_space/M_structure.lean

Modified src/data/list/func.lean

modified theorem list.func.nil_sub

modified theorem list.func.sub_nil

Modified src/field_theory/separable_degree.lean

Modified src/linear_algebra/bilinear_form.lean

Modified src/logic/equiv/list.lean

modified def equiv.list_equiv_self_of_equiv_nat

Modified src/measure_theory/integral/circle_transform.lean

Modified src/model_theory/elementary_maps.lean

modified theorem first_order.language.elementary_embedding.map_bounded_formula

modified theorem first_order.language.elementary_embedding.map_formula

Modified src/number_theory/legendre_symbol/gauss_sum.lean

modified theorem char.card_pow_card

Modified src/number_theory/legendre_symbol/quadratic_char.lean

modified theorem quadratic_char_card_card