Pascal's Triangle and Lucas's Theorem

被引：0
|
作者：
Ziobro, Rafal [1 ]
机构：
[1] Univ Agr, Dept Carbohydrate Technol & Cereal Proc, Krakow, Poland
来源：
FORMALIZED MATHEMATICS | 2024年 / 32卷 / 01期
关键词：
arithmetic triangle; binomial coefficient; Lucas theorem;
D O I：
10.2478/forma-2024-0020
中图分类号：
O1 [数学];
学科分类号：
0701 ; 070101 ;
摘要：
In this article we construct formally the Pascal's triangle using Mizar proof assistant. Using the same techniques, we show some similar constructions based on integer sequences. We also prove Lucas's theorem providing useful registrations of clusters to enable more automation in calculations.
引用
收藏
页码：235 / 245
页数：11
相关论文
共 50 条
  • [1] An extension of Lucas identity via Pascal's triangle
    Anatriello, Giuseppina
    Vineenzi, Giovanni
    HACETTEPE JOURNAL OF MATHEMATICS AND STATISTICS, 2021, 50 (03): : 647 - 658
  • [2] ON A GENERALIZATION OF A LUCAS' RESULT ON THE PASCAL'S TRIANGLE AND MERSENNE NUMBERS
    Yamagami, Atsushi
    Harada, Hideyuki
    JP JOURNAL OF ALGEBRA NUMBER THEORY AND APPLICATIONS, 2019, 42 (02): : 159 - 169
  • [3] On a Generalization of a Lucas' Result and an Application to the 4-Pascal's Triangle
    Yamagami, Atsushi
    Taniguchi, Kazuki
    SYMMETRY-BASEL, 2020, 12 (02):
  • [4] A new configurable decimation filter using Pascal's triangle theorem
    Cherik Chahardah, A.
    Farshidi, E.
    World Academy of Science, Engineering and Technology, 2011, 78 : 75 - 78
  • [5] The backbone of Pascal's triangle
    Baylis, John
    MATHEMATICAL GAZETTE, 2010, 94 (529): : 184 - 185
  • [6] Pascal's Triangle of Configurations
    Gevay, Gabor
    DISCRETE GEOMETRY AND SYMMETRY: DEDICATED TO KAROLY BEZDEK AND EGON SCHULTE ON THE OCCASION OF THEIR 60TH BIRTHDAYS, 2018, 234 : 181 - 199
  • [7] Extended Pascal's triangle
    Atanassov, Krassimir T.
    NOTES ON NUMBER THEORY AND DISCRETE MATHEMATICS, 2016, 22 (01) : 55 - 58
  • [8] Pascal's Theorem
    Tabirca, Sabin
    AMERICAN MATHEMATICAL MONTHLY, 2016, 123 (10): : 1052 - 1052
  • [9] Pascal's triangle (mod 9)
    Huard, JG
    Spearman, BK
    Williams, KS
    ACTA ARITHMETICA, 1997, 78 (04) : 331 - 349
  • [10] Pascal's triangle (mod 8)
    Huard, JG
    Spearman, BK
    Williams, KS
    EUROPEAN JOURNAL OF COMBINATORICS, 1998, 19 (01) : 45 - 62
12345