| Ovaj članak ili neki od njegovih odlomaka nije dovoljno potkrijepljen izvorima (literatura, veb-sajtovi ili drugi izvori). Ako se pravilno ne potkrijepe pouzdanim izvorima, sporne rečenice i navodi mogli bi biti izbrisani. Pomozite Wikipediji tako što ćete navesti validne izvore putem referenci te nakon toga možete ukloniti ovaj šablon. |
U algebri, Leibnizova formula izražava determinantu kvadratne matrice
preko permutacija elemenata te matrice. Naziv je dobila prema njemačkom matematičaru Gottfriedu Leibnizu, a formula glasi:

za matricu dimenzije n×n, gdje je sgn sgn funkcija ili permutacije u permutacionoj grupi Sn, koja daje razultat +1 i −1 za parne i neparne permutacije, respektivno.
Druga uobičajna notacija, koja se koristi za ovu formulu, je preko Levi-Civitaovog simbola, te koristi Einsteinovu notaciju, kada postoje:

što je poznatije fizičarima.
Teorem
Postoji tačno jedna funkcija

koja je alternativno multilinearno prema kolonama, takvo da je
.
Dokaz
Jedinstvenost: Neka
bude funkcija, i neka
bude matrica dimenzije
. Reći ćemo da je
-ta kolona matrice
, to jest
, takvo da je
Također, neka
označava
-tu vektor kolonu matrice identiteta.
Tada se piše svaki
član kao
, to jest
.
Pošto je
multilinearno, imamo da je

Iz alternacije, slijedi da ako je
, tada imamo

Pošto gornja suma uzima u obzir sve moguće šanse poredanih
-tostrukosti
, i pošto
implicira da je F nula, suma se može redukovati iz mnogostrukosti do permutacija kao

Pošto je F alternativno, kolone
se mogu zamijenjivati dok ne postane identitet. Sgn funkcija
definisana je da broji broj zamijena neophodnih, te da uračuna rezultirajuću promjenu znaka. Na kraju se dobija:

gdje
treba da bude jednako
.
Zbog toga, ni jedna funkcija pored funkcije definisane preko Leibnizove formule nije multilinearna alternativna funkcija sa
.
Postojanje: Sada ćemo pokazati da F, gdje je F funkcija definisana preko Leibnizove formule, ima tri osobine.
Multilinearnost:

Alternativnost:

Sad neka
bude mnogostrukost jednaka
sa zamijenjenim indeksima
i
. Slijedi iz definicije
funkcije da je
.

Konačno,
:

Zbog toga samo funkcije, koje su multilinearno alternativne s
, su ograničene na funkcije koje su definisane Leibnizovom formulom, koja i sama ima tri osobine. Zbog toga determinanta može biti definisana kao jedina funkcija

sa ove tri osobine.
- Lloyd N. Trefethen and David Bau, Numerical Linear Algebra (SIAM, 1997).