LocalInv
📁 Source: ClassFieldTheory/Cohomology/LocalInv.lean
Statistics
(root)
Definitions
| Name | Category | Theorems |
|---|---|---|
carry 📖 | CompOp | |
carryCocycle 📖 | CompOp | |
carryH2Aux 📖 | CompOp | |
localInv 📖 | CompOp | |
localInvAux 📖 | CompOp | |
localInvAuxAux 📖 | CompOp | — |
localInvIso 📖 | CompOp |
Theorems
| Name | Kind | Assumes | Proves | Validates | Depends On |
|---|---|---|---|---|---|
carryCocycle_apply 📖 | mathematical | — | carryCocyclecarry | — | — |
carry_add_carry_add_left 📖 | mathematical | — | carry | — | carry.eq_1 |
carry_add_carry_add_right 📖 | mathematical | — | carry | — | carry_commcarry_add_carry_add_left |
carry_comm 📖 | mathematical | — | carry | — | — |
carry_eq_ite 📖 | mathematical | — | carry | — | — |
carry_neg_one_one 📖 | mathematical | — | carry | — | carry_eq_ite |
carry_one_right_of_ne_neg_one 📖 | mathematical | — | carry | — | carry_eq_ite |
leftInverse_carryH2Aux_localInvAux 📖 | mathematical | — | carryH2AuxlocalInvAux | — | rightInverse_carryH2Aux_localInvAux |
localInvIso_hom_hom_apply 📖 | mathematical | — | localInvIsolocalInv | — | — |
localInvIso_inv_hom_apply 📖 | mathematical | — | localInvIsolocalInv | — | — |
localInv_H2π_hom 📖 | mathematical | — | localInv | — | groupCohomology.H2π_comp_H2Iso_hom_apply |
localInv_symm_apply 📖 | mathematical | — | localInvcarryCocycle | — | — |
rightInverse_carryH2Aux_localInvAux 📖 | mathematical | — | carryH2AuxlocalInvAux | — | — |
---