Commit 2024-11-15 20:09 4cfdb02b

View on Github →

feat(Analysis/InnerProductSpace/Dual, Analysis/Normed/Group/SeparationQuotient): add null subspaces (#16707) Define the null submodule in an InnerProductSpace and the null subgroup in a NormedAddCommGroup and prove basic properties. ~~Define the null space in an InnerProductSpace without definite and add InnerProduceSpace structure to the quotient by the null space.~~ Motivation: This PR has evolved from a PR defining the SeparationQuotient for InnerProductSpace. That has been done in #17452 and now contains some other things.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Analysis/InnerProductSpace/Basic.lean

added theorem inner_eq_zero_of_left

added theorem inner_eq_zero_of_right

Modified Mathlib/Analysis/InnerProductSpace/Dual.lean

added theorem InnerProductSpace.nullSubmodule_le_ker_toDualMap_left

added theorem InnerProductSpace.nullSubmodule_le_ker_toDualMap_right

Modified Mathlib/Analysis/Normed/Group/Basic.lean

added theorem nnnorm_div_eq_nnnorm_left

added theorem nnnorm_div_eq_nnnorm_right

added theorem nnnorm_le_mul_nnnorm_add'

added theorem nnnorm_mul_eq_nnnorm_left

added theorem nnnorm_mul_eq_nnnorm_right

added theorem norm_div_eq_norm_left

added theorem norm_div_eq_norm_right

added theorem norm_le_mul_norm_add'

added theorem norm_mul_eq_norm_left

added theorem norm_mul_eq_norm_right

Created Mathlib/Analysis/Normed/Group/NullSubmodule.lean

added theorem isClosed_nullSubgroup

added theorem isClosed_nullSubmodule

added theorem mem_nullSubgroup_iff

added theorem mem_nullSubmodule_iff

added def nullSubgroup

added def nullSubmodule

Modified Mathlib/Analysis/Normed/Group/Uniform.lean

added theorem SeparationQuotient.mk_eq_one_iff