mathlib

73aaf32e - refactor(algebraic_geometry/EllipticCurve): refactor base change and variable change (#17708)

refactor(algebraic_geometry/EllipticCurve): refactor base change and variable change (#17708) Add `simps` for `base_change` and `variable_change` (renamed from `change_of_variable` for consistency), rename `simp` lemmas and squeeze their proofs. Includes #17700