Commit 2023-11-18 01:09 b0e957dd

View on Github →

fix: remove remaining ^ fixes (#8463)

Estimated changes

Modified Archive/Imo/Imo2020Q2.lean

Modified Counterexamples/CliffordAlgebra_not_injective.lean

Modified Mathlib/Algebra/Module/Submodule/LinearMap.lean

Modified Mathlib/Algebra/Quaternion.lean

modified theorem Cardinal.mk_quaternion

modified theorem Cardinal.mk_quaternionAlgebra

modified theorem Cardinal.mk_univ_quaternion

modified theorem Cardinal.mk_univ_quaternionAlgebra

Modified Mathlib/Analysis/NormedSpace/Spectrum.lean

Modified Mathlib/Data/Complex/Basic.lean

Modified Mathlib/LinearAlgebra/TensorAlgebra/Basis.lean

Modified Mathlib/MeasureTheory/Constructions/HaarToSphere.lean

Modified Mathlib/MeasureTheory/Function/UniformIntegrable.lean

Modified Mathlib/MeasureTheory/Measure/Hausdorff.lean

Modified Mathlib/NumberTheory/NumberField/CanonicalEmbedding.lean

Modified Mathlib/NumberTheory/NumberField/Discriminant.lean

Modified Mathlib/NumberTheory/NumberField/Units.lean

Modified Mathlib/SetTheory/Cardinal/Basic.lean

modified theorem Cardinal.mk_finset_of_fintype

modified theorem Cardinal.mk_list_eq_sum_pow

modified theorem Cardinal.mk_vector

modified theorem Cardinal.pow_cast_right

Modified Mathlib/SetTheory/Cardinal/Cofinality.lean

Modified Mathlib/SetTheory/Cardinal/Ordinal.lean

modified theorem Cardinal.power_nat_eq

modified theorem Cardinal.power_nat_le

Modified Mathlib/SetTheory/Ordinal/Notation.lean

Modified test/norm_cast.lean