Skip to content

Instantly share code, notes, and snippets.

View ammkrn's full-sized avatar

Chris Bailey ammkrn

50 followers · 4 following
View GitHub Profile
@ammkrn
ammkrn / sus_mv_polynomial.total_degree_mul.lean
Created March 8, 2021 03:28
c8892e44 mv_polynomial.total_degree_mul
lemma {u u_1} mv_polynomial.total_degree_mul {R : Type u} {σ : Type u_1}
[inst_1 : comm_semiring R] (a b : mv_polynomial σ R) :
mv_polynomial.total_degree (a * b) ≤
mv_polynomial.total_degree a + mv_polynomial.total_degree b :=
finset.sup_le
(λ (n : σ →₀ nat) (hn : n ∈ finsupp.support (a * b)),
(λ (this :
n ∈
finset.bUnion (finsupp.support a)
(λ (a₁ : σ →₀ nat),
@ammkrn
ammkrn / private_fork.md
Created September 24, 2020 15:47 — forked from 0xjac/private_fork.md
Create a private fork of a public repository

The repository for the assignment is public and Github does not allow the creation of private forks for public repositories.

The correct way of creating a private frok by duplicating the repo is documented here.

For this assignment the commands are:

  1. Create a bare clone of the repository. (This is temporary and will be removed so just do it wherever.) 
    

    2. 



git clone --bare git@github.com:usi-systems/easytrace.git



  


  




    


          
    

      

        
        

          

              @ammkrn
          

          

            
                ammkrn
                / mathlib_high_scores
            
            

              Last active
              August 11, 2020 21:54
            

              
                mathlib_high_scores
              
          

        

      

        

  

    
    


        



  


  

        

          
          #### SIZE (GARBAGE LEAN OBJECTS)
        

        

          
          10794778 : polynomial.monic.next_coeff_mul 
        

        

          
          1090313 : composition_as_set_equiv._proof_5 
        

        

          
          662922 : real.pi_lt_3141593 
        

        

          
          468943 : real.pi_gt_3141592 
        

        

          
          413365 : real.pi_lt_31416 
        

        

          
          342992 : sum_range_choose_halfway 
        

        

          
          315037 : _private.4086404821.sum_four_squares_of_two_mul_sum_four_squares 
        

        

          
          263176 : polynomial.irreducible_of_eisenstein_criterion 
        

        

          
          228696 : AddCommGroup.kernel_iso_ker_over._proof_4