Skip to content
Started 1 yr 5 mo ago
Took 20 min on workermtahpc
Success

#3996 (Oct 3, 2022, 1:14:04 PM)

Changes

Mercurial (hg https://foss.heptapod.net/isa-afp/afp-devel/ default)

  1. Many changes to entry `Complex_Bounded_Operators`:
    - Removed all use of deprecated `⟨.,.⟩` syntax for complex inner product. (Now: `∙⇩C`)
    - Cosmetic changes and cleanup of some proofs
    - Type class `one_dim` inherits from `complex_inner` now.
    - Moved various theorems around between theories
    - Added `[simp]` to: `Proj_partial_isometry`, `cadjoint_id`
    - Removed theorems: `onorm_Inf_bound`, `norm_unit_sphere`
    - Changed theorems: `of_complex_cblinfun_apply` (made into more general simp-rule), TODO orthospacething
    - New definition: `rank1` (and lemmas about it)
    - New theorems: `one_dim_iso_cblinfun_apply`, `vector_to_cblinfun_one_dim_iso`, `image_vector_to_cblinfun_adj`,
      `image_vector_to_cblinfun_adj'`, `sgn_cinner`, `orthocomplement_top`, `orthogonal_spaces_ccspan`, `norm_scaleC_sgn`,
      `one_dim_ccsubspace_all_or_nothing`, `surj_isometry_is_unitary`
    - Renamed `vector_to_cblinfun_cblinfun_apply` -> `vector_to_cblinfun_cblinfun_compose` (also turned around and added `[simp]`),
      `cancel_apply_Proj` -> `Proj_fixes_image`, `range_is_clinear` -> `range_is_csubspace`.
    - Changed definition: `is_Proj` (logically equivalent by `Proj_range_closed`)

    Fixed entry `Registers` due to the changes above. (detail)

Started by an SCM change

This run spent:

  • 2 min 2 sec waiting;
  • 20 min build duration;
  • 22 min total from scheduled to completion.
Revision: 6ab4bb7cb8b2cb6d85c564b75fa29cef0aace417
Revision: 1145c2ed8f6c99ebd9c6711a59f3a4d226c9bfbb