Mathlib Changelog
v3
Changelog
About
Github
Mathlib v3 is deprecated.
Go to Mathlib v4
Commit
2020-07-19 04:53
e6bfe187
View on Github →
feat(topology/algebra/module): pi and proj for CLM (
#3430
)
Estimated changes
Modified
src/topology/algebra/module.lean
added
theorem
continuous_linear_map.infi_ker_proj
added
def
continuous_linear_map.infi_ker_proj_equiv
added
def
continuous_linear_map.pi
added
theorem
continuous_linear_map.pi_apply
added
theorem
continuous_linear_map.pi_comp
added
theorem
continuous_linear_map.pi_eq_zero
added
theorem
continuous_linear_map.pi_zero
added
def
continuous_linear_map.proj
added
theorem
continuous_linear_map.proj_apply
added
theorem
continuous_linear_map.proj_pi