{-# LANGUAGE NoImplicitPrelude #-}

-- |
-- Module      : OAlg.AbelianGroup.Proposition
-- Description : validity of abelian groups
-- Copyright   : (c) Erich Gut
-- License     : BSD3
-- Maintainer  : zerich.gut@gmail.com
--
-- validity of abelian groups.
module OAlg.AbelianGroup.Proposition
  ( prpAbelianGroups
  ) where

import OAlg.Prelude
import OAlg.AbelianGroup.KernelsAndCokernels

-- | validity for abelian groups.
prpAbelianGroups :: Statement
prpAbelianGroups :: Statement
prpAbelianGroups = String -> Label
Prp String
"AbelianGroups"
  Label -> Statement -> Statement
:<=>: [Statement] -> Statement
And [ String -> Label
Label String
"isoSmithNormal" Label -> Statement -> Statement
:<=>: X AbGroup -> (AbGroup -> Statement) -> Statement
forall x. X x -> (x -> Statement) -> Statement
Forall X AbGroup
forall x. XStandard x => X x
xStandard (Inv AbHom -> Statement
forall a. Validable a => a -> Statement
valid (Inv AbHom -> Statement)
-> (AbGroup -> Inv AbHom) -> AbGroup -> Statement
forall y z x. (y -> z) -> (x -> y) -> x -> z
forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. AbGroup -> Inv AbHom
isoSmithNormal)
            , String -> Label
Label String
"kernels" Label -> Statement -> Statement
:<=>: Kernels N1 AbHom -> Statement
forall a. Validable a => a -> Statement
valid Kernels N1 AbHom
abhKernels
            ]