------------------------------------------------------------------------
-- The Agda standard library
--
-- The Binomial Theorem for Commutative Semirings
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --safe #-}
open import Algebra.Bundles using (CommutativeSemiring)
module Algebra.Properties.CommutativeSemiring.Binomial {a ℓ} (S : CommutativeSemiring a ℓ) where
open CommutativeSemiring S
open import Algebra.Properties.Semiring.Exp semiring using (_^_)
import Algebra.Properties.Semiring.Binomial semiring as Binomial
open Binomial public hiding (theorem)
------------------------------------------------------------------------
-- Here it is
theorem : ∀ n x y → (x + y) ^ n ≈ binomialExpansion x y n
theorem n x y = Binomial.theorem x y (*-comm x y) n
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4