Commit 2024-07-11 11:51 9c8f4234

View on Github →

chore: make Algebra.cast reducible (#14601) Make Algebra.cast @[reducible]

Estimated changes

Modified Mathlib/Algebra/Algebra/Defs.lean

modified def Algebra.cast

Modified Mathlib/Algebra/Algebra/Field.lean

modified theorem algebraMap.lift_map_eq_zero_iff

Modified Mathlib/Analysis/InnerProductSpace/Basic.lean

Modified Mathlib/Analysis/InnerProductSpace/OfNorm.lean

Modified Mathlib/Analysis/InnerProductSpace/Projection.lean

Modified Mathlib/Analysis/InnerProductSpace/TwoDim.lean

Modified Mathlib/Analysis/RCLike/Basic.lean

Modified Mathlib/Analysis/SpecialFunctions/Pow/Real.lean