Documentation Verification Report

Hilbert90

📁 Source: Mathlib/RepresentationTheory/Homological/GroupCohomology/Hilbert90.lean

Statistics

Metric	Count
Definitions `H1ofAutOnUnitsUnique`, `aux`	2
Theorems `aux_ne_zero`, `exists_div_of_norm_eq_one`, `exists_mul_galRestrict_of_norm_eq_one`, `isMulCoboundary₁_of_isMulCocycle₁_of_aut_to_units`, `norm_ofAlgebraAutOnUnits_eq`	5
Total	7

groupCohomology

Definitions

Name	Category	Theorems
`H1ofAutOnUnitsUnique` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_div_of_norm_eq_one` 📖	mathematical	`AlgEquiv` `Semifield.toCommSemiring` `Field.toSemifield` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Subgroup` `AlgEquiv.aut` `SetLike.instMembership` `Subgroup.instSetLike` `Subgroup.zpowers` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `DivisionRing.toRing` `Field.toDivisionRing` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `MonoidHom.instFunLike` `Algebra.norm` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne`	`DivInvMonoid.toDiv` `DivisionRing.toDivInvMonoid` `Units.val` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `AlgEquiv.instFunLike`	—	`Ne.isUnit` `Algebra.norm_ne_zero_iff` `instIsDomain` `Module.free_of_finite_type_torsion_free'` `EuclideanDomain.to_principal_ideal_domain` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `zero_ne_one` `NeZero.one` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `norm_ofAlgebraAutOnUnits_eq` `RingHomSurjective.ids` `Rep.FiniteCyclicGroup.groupCohomologyπOdd_eq_zero_iff` `Unique.instSubsingleton` `div_eq_mul_inv` `AlgHomClass.toRingHomClass` `AlgEquivClass.toAlgHomClass` `AlgEquiv.instAlgEquivClass` `sub_eq_add_neg` `Mathlib.Tactic.TermCongr.cHole.congr_simp` `map_add` `AddMonoidHomClass.toAddHomClass` `AddEquivClass.instAddMonoidHomClass` `AddEquiv.instAddEquivClass` `map_neg` `Units.val_inv_eq_inv_val` `Units.ext_iff` `Algebra.norm_inv` `inv_one` `IsUnit.div_eq_iff` `Units.isUnit` `Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq` `IsCancelMulZero.toIsLeftCancelMulZero` `instIsCancelMulZero` `Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval` `Mathlib.Tactic.FieldSimp.NF.atom_eq_eval` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval` `Mathlib.Tactic.FieldSimp.NF.inv_eq_eval` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₁` `one_mul` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval₂` `Mathlib.Tactic.FieldSimp.NF.one_div_eq_eval` `Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons` `Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons_zero` `Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero` `Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst` `Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div` `div_one` `Mathlib.Tactic.FieldSimp.NF.eval_cons` `Mathlib.Tactic.FieldSimp.zpow'_one` `one_ne_zero` `GroupWithZero.toNontrivial`
`exists_mul_galRestrict_of_norm_eq_one` 📖	mathematical	`AlgEquiv` `Semifield.toCommSemiring` `Field.toSemifield` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Subgroup` `AlgEquiv.aut` `SetLike.instMembership` `Subgroup.instSetLike` `Subgroup.zpowers` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `DivisionRing.toRing` `Field.toDivisionRing` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `MonoidHom.instFunLike` `Algebra.norm` `RingHom` `RingHom.instFunLike` `algebraMap` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne`	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `AlgEquiv.instFunLike` `MulEquiv` `MulOne.toMul` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `galRestrict` `Algebra.IsSeparable.isAlgebraic` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `IsGalois.to_isSeparable`	—	`Module.isTorsionFree_iff_algebraMap_injective` `instIsDomain` `IsScalarTower.algebraMap_eq` `RingHom.injective` `DivisionRing.isSimpleRing` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `IsFractionRing.injective` `IsIntegralClosure.isLocalization` `Algebra.IsSeparable.isAlgebraic` `IsGalois.to_isSeparable` `Algebra.norm_zero` `Module.free_of_finite_type_torsion_free'` `EuclideanDomain.to_principal_ideal_domain` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `NeZero.one` `exists_div_of_norm_eq_one` `IsLocalization.exists_mk'_eq` `Subtype.prop` `Algebra.smul_def` `IsScalarTower.algebraMap_apply` `IsLocalization.mk'_spec'` `zero_ne_one` `IsLocalization.mk'_zero` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `AlgHomClass.toRingHomClass` `AlgEquivClass.toAlgHomClass` `AlgEquiv.instAlgEquivClass` `div_zero` `eq_div_iff_mul_eq` `zero_div` `map_eq_zero` `IsIntegralClosure.algebraMap_injective` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `RingHom.instRingHomClass` `AlgHom.map_smul_of_tower` `LinearMap.IsScalarTower.compatibleSMul` `AlgEquiv.toAlgHom_apply` `mul_left_comm` `algebraMap_galRestrictHom_apply`
`isMulCoboundary₁_of_isMulCocycle₁_of_aut_to_units` 📖	mathematical	`IsMulCocycle₁` `AlgEquiv` `Semifield.toCommSemiring` `Field.toSemifield` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Units` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `AlgEquiv.aut` `Units.instCommGroupUnits` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction` `MulDistribMulAction.toMulAction` `Units.instMonoid` `AlgEquiv.instMulDistribMulActionUnits`	`IsMulCoboundary₁`	—	`Hilbert90.aux_ne_zero` `Finsupp.sum_fintype` `zero_smul` `Finset.sum_congr` `Finset.sum_apply` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `AlgHomClass.toRingHomClass` `AlgEquivClass.toAlgHomClass` `AlgEquiv.instAlgEquivClass` `map_inv` `MonoidHom.instMonoidHomClass` `div_inv_eq_mul` `map_sum` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `map_mul` `NonUnitalAlgSemiHomClass.toMulHomClass` `Finset.sum_mul` `mul_assoc` `mul_comm` `Fintype.sum_bijective` `Group.mulLeft_bijective`
`norm_ofAlgebraAutOnUnits_eq` 📖	mathematical	—	`Units.val` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DFunLike.coe` `Equiv` `Additive` `Units` `EquivLike.toFunLike` `Equiv.instEquivLike` `Additive.toMul` `AddEquiv` `ModuleCat.carrier` `CommRing.toRing` `Int.instCommRing` `Action.V` `ModuleCat` `ModuleCat.moduleCategory` `AlgEquiv` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `AlgEquiv.aut` `Rep.ofMulDistribMulAction` `Units.instCommGroupUnits` `CommRing.toCommMonoid` `AlgEquiv.instMulDistribMulActionUnits` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `Rep.instAddCommGroupCarrierVModuleCat` `Additive.add` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommGroup.toGroup` `AddEquiv.instEquivLike` `Rep.toAdditive` `Rep.ofAlgebraAutOnUnits` `CategoryTheory.ConcreteCategory.hom` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `ModuleCat.isAddCommGroup` `ModuleCat.isModule` `LinearMap.instFunLike` `ModuleCat.instConcreteCategoryLinearMapIdCarrier` `Action.Hom.hom` `Rep.norm` `AlgEquiv.fintype` `AddEquiv.symm` `Additive.ofMul` `RingHom` `Semifield.toCommSemiring` `Field.toSemifield` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `RingHom.instFunLike` `algebraMap` `MonoidHom` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `DivisionRing.toRing` `Field.toDivisionRing` `MonoidHom.instFunLike` `Algebra.norm`	—	`MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `AlgHomClass.toRingHomClass` `AlgEquivClass.toAlgHomClass` `AlgEquiv.instAlgEquivClass` `LinearMap.coe_sum` `Finset.sum_apply` `Finset.sum_congr` `map_sum` `AddEquivClass.instAddMonoidHomClass` `AddEquiv.instAddEquivClass` `Finset.prod_congr` `Units.coe_prod` `Algebra.norm_eq_prod_automorphisms`

groupCohomology.Hilbert90

Definitions

Name	Category	Theorems
`aux` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`aux_ne_zero` 📖	—	—	—	—	`LinearIndependent.comp` `linearIndependent_monoidHom` `instIsDomain` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `AlgHomClass.toRingHomClass` `AlgEquivClass.toAlgHomClass` `AlgEquiv.instAlgEquivClass` `AlgEquiv.ext` `DFunLike.ext_iff` `linearIndependent_iff` `Units.ne_zero` `IsLocalRing.toNontrivial` `Field.instIsLocalRing`

---

← Back to Index