| Name | Category | Theorems |
|---|
Basis3 📖 | CompOp | 1 mathmath: cob_mat_other_repr
|
COB 📖 | CompOp | 3 mathmath: COB_to_basis, cob_mat_other_repr, inner_as_to_matrix
|
COB_MB 📖 | CompOp | 3 mathmath: COB_MB_is_ortho, COB_to_basis, inner_as_to_matrix_MB
|
COB_mat 📖 | CompOp | 2 mathmath: COB_mat_is_ortho, cob_mat_other_repr
|
PROD_BLOCK 📖 | CompOp | — |
ang_diff 📖 | CompOp | 2 mathmath: BadAtN_rot_iso_equiv, rot_iso_fixed_gen
|
ax_B 📖 | CompOp | — |
ax_space 📖 | CompOp | — |
choice_set 📖 | CompOp | 1 mathmath: orth_nonempty
|
fTS_fun 📖 | CompOp | 1 mathmath: fTS_fun_bij
|
finToSigma 📖 | CompOp | — |
mod_dim 📖 | CompOp | 4 mathmath: block_1_lem, fTS_fun_bij, block_repr, block_2_lem
|
mod_dim_decidableEq 📖 | CompOp | 3 mathmath: block_1_lem, block_repr, block_2_lem
|
mod_dim_fintype 📖 | CompOp | 3 mathmath: block_1_lem, block_repr, block_2_lem
|
operp 📖 | CompOp | 7 mathmath: operp_of_ax_space, operp_up_2, operp_add, spar_operp, el_by_parts, operp_up, operp_spar
|
orth 📖 | CompOp | 14 mathmath: spar_up_rot, orth_nonempty, orth_dim_2, spar_up_2, operp_of_ax_space, rips_add, operp_up_2, triv_rot_inner, up_mem, operp_add, spar_operp, el_by_parts, operp_up, operp_spar
|
orth_B 📖 | CompOp | — |
plane_o 📖 | CompOp | — |
rot 📖 | CompOp | 8 mathmath: countable_bad_rots, rot_containment_general, bad_as_union_rot, triv_rot, rot_pow_lemma, rot_comp_add, same_action, rot_containment_S2
|
rot_by_parts 📖 | CompOp | 2 mathmath: triv_rot_by_parts, rot_by_parts_comp
|
rot_iso 📖 | CompOp | 13 mathmath: rot_iso_pow_lemma, hf, rot_iso_fixed_back, rot_iso_comp_add, triv_rot_iso, block_1_lem, same_action, inner_as_to_matrix_MB, inner_as_to_matrix, rot_iso_power_lemma, block_repr, rot_iso_comp, block_2_lem
|
rot_iso_plane_equiv 📖 | CompOp | — |
rot_iso_plane_to_st 📖 | CompOp | 2 mathmath: rips_add, triv_rot_inner
|
rot_mat 📖 | CompOp | 2 mathmath: rot_mat_is_special, rot_mat_comp_add
|
rot_mat_block_1 📖 | CompOp | 1 mathmath: rot_mat_block_prop
|
rot_mat_block_2 📖 | CompOp | 1 mathmath: rot_mat_block_prop
|
rot_mat_inner 📖 | CompOp | 5 mathmath: rmi_trans_equiv, rot_mat_inner_is_special, rot_mat_inner_comp_add, inner_as_to_matrix_MB, inner_as_to_matrix
|
rot_mat_inner_trans 📖 | CompOp | 1 mathmath: rmi_trans_equiv
|
sm_bases 📖 | CompOp | 3 mathmath: block_1_lem, block_repr, block_2_lem
|
spar 📖 | CompOp | 9 mathmath: spar_up_rot, spar_add, spar_up_2, spar_of_ax_space, spar_of_orth, spar_operp, spar_spar, el_by_parts, operp_spar
|
submods 📖 | CompOp | 5 mathmath: hf, internal_pr, block_1_lem, block_repr, block_2_lem
|
tmp_basis 📖 | CompOp | — |
up 📖 | CompOp | 3 mathmath: spar_up_rot, up_mem, operp_up
|
x_B 📖 | CompOp | — |
x_B_c 📖 | CompOp | — |