Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-08-21 19:16 90bc9579

View on Github →

chore(analysis/inner_product_space): move is_symmetric to a new file lower in the import tree (#16106)

Estimated changes

Modified src/analysis/inner_product_space/adjoint.lean

deleted theorem linear_map.is_symmetric.add

deleted theorem linear_map.is_symmetric.apply_clm

deleted theorem linear_map.is_symmetric.coe_re_apply_inner_self_apply

deleted theorem linear_map.is_symmetric.conj_inner_sym

deleted theorem linear_map.is_symmetric.continuous

deleted theorem linear_map.is_symmetric.restrict_invariant

deleted theorem linear_map.is_symmetric.restrict_scalars

deleted def linear_map.is_symmetric

deleted theorem linear_map.is_symmetric_id

deleted theorem linear_map.is_symmetric_iff_bilin_form

deleted theorem linear_map.is_symmetric_iff_inner_map_self_real

deleted theorem linear_map.is_symmetric_zero

deleted theorem orthogonal_projection_is_symmetric

Modified src/analysis/inner_product_space/projection.lean

added theorem orthogonal_projection_is_symmetric

Created src/analysis/inner_product_space/symmetric.lean

added theorem linear_map.is_symmetric.add

added theorem linear_map.is_symmetric.apply_clm

added theorem linear_map.is_symmetric.coe_re_apply_inner_self_apply

added theorem linear_map.is_symmetric.conj_inner_sym

added theorem linear_map.is_symmetric.continuous

added theorem linear_map.is_symmetric.restrict_invariant

added theorem linear_map.is_symmetric.restrict_scalars

added def linear_map.is_symmetric

added theorem linear_map.is_symmetric_id

added theorem linear_map.is_symmetric_iff_bilin_form

added theorem linear_map.is_symmetric_iff_inner_map_self_real

added theorem linear_map.is_symmetric_zero