Commit 2023-09-11 20:08 a4810ea0

View on Github →

feat (NormedSpace.Dual): make Dual reducible (#6998) Following LinearAlgebra.Dual this makes NormedSpace.Dual reducible.

Estimated changes

Modified Mathlib/Analysis/InnerProductSpace/Adjoint.lean

deleted def ContinuousLinearMap.adjointAux

Modified Mathlib/Analysis/InnerProductSpace/Dual.lean

Modified Mathlib/Analysis/InnerProductSpace/LinearPMap.lean

Modified Mathlib/Analysis/NormedSpace/Dual.lean

deleted def NormedSpace.Dual

Modified docs/undergrad.yaml