Def ContinuousLinearMap.adjointAux

Modification history

2026-06-03 01:29

Mathlib/Analysis/InnerProductSpace/Adjoint.lean

chore(Analysis/InnerProductSpace): make `adjointAux` private (#40091)

Added ContinuousLinearMap.adjointAux View on Github →

2023-09-11 20:08

Mathlib/Analysis/InnerProductSpace/Adjoint.lean

feat (NormedSpace.Dual): make `Dual` reducible (#6998) …

Deleted ContinuousLinearMap.adjointAux View on Github →

2023-06-01 13:13

Mathlib/Analysis/InnerProductSpace/Adjoint.lean

feat: port Analysis.InnerProductSpace.Adjoint (#4476)

Added ContinuousLinearMap.adjointAux View on Github →