Mathlib Changelog
v3
Changelog
About
Github
Mathlib v3 is deprecated.
Go to Mathlib v4
Commit
2021-08-15 23:17
8e508633
View on Github →
chore(analysis/normed_space/dual): golf some proofs (
#8694
)
Estimated changes
Modified
src/analysis/normed_space/dual.lean
modified
theorem
normed_space.double_dual_bound
modified
theorem
normed_space.dual_def
deleted
def
normed_space.inclusion_in_double_dual'
added
theorem
normed_space.inclusion_in_double_dual_norm_eq
added
theorem
normed_space.inclusion_in_double_dual_norm_le