Commit 2023-06-12 01:02 5068808d

View on Github →

chore: formatting issues (#4947)

Estimated changes

modified theorem AlgEquiv.aut_mul
modified theorem AlgEquiv.aut_one
modified theorem FreeAddMonoid.countp_of
modified theorem Units.exists0
modified theorem isPrimePow_def
modified theorem isPrimePow_iff_pow_succ
modified theorem Int.preimage_ceil_singleton
modified theorem PUnit.norm_unit_eq
modified theorem star_ofNat
modified theorem exists_hilbertBasis
modified theorem mem_balancedHull_iff
modified theorem FintypeCat.hom_ext
modified theorem Finset.mem_upShadow_iff
modified theorem Bool.eq_iff_eq_true_iff
modified theorem Finset.coe_pow
modified theorem Finset.coe_zpow
modified def Ordnode.repr
modified theorem Function.extend_mul
modified theorem NNReal.toReal_le_toReal
modified def Computation.orElse
modified theorem Set.image2_inter_left
modified theorem Set.image2_inter_right
modified theorem Setoid.classes_eqv_classes
modified theorem Setoid.eq_eqv_class_of_mem
modified theorem Setoid.eq_of_mem_eqv_class
modified theorem Setoid.eqv_class_mem'
modified theorem Setoid.eqv_class_mem
modified theorem Setoid.eqv_classes_disjoint
modified def Setoid.mkClasses
modified theorem String.length_replicate
modified theorem Sum.getLeft_map
modified theorem Sum.isLeft_map
modified theorem Sum.isRight_map
modified theorem Sym.exists_eq_cons_of_succ
modified theorem Vector.exists_eq_cons
modified theorem Vector3.consElim_cons
modified theorem ZMod.int_cast_rightInverse
modified theorem FiniteField.card'
modified theorem FreeGroup.reduce.not
modified theorem FreeProduct.NeWord.of_word
modified theorem Equiv.pow_addLeft
modified theorem Equiv.pow_addRight
modified theorem Equiv.pow_mulLeft
modified theorem Equiv.pow_mulRight
modified theorem Subgroup.mem_sup'
modified theorem max_eq_left
modified theorem max_eq_right
modified theorem min_assoc
modified theorem min_eq_left
modified theorem min_eq_right
modified def Lean.Expr.getArg?
modified theorem Submodule.mem_sup'
modified theorem Encodable.decode_one
modified theorem Function.hfunext
modified theorem Module.Finite.exists_fin
modified theorem multiplicity.finite_mul_aux
modified def WittVector.mk
modified theorem Cardinal.ord_eq
modified theorem Ordinal.toNatOrdinal_max
modified def cancelDenominatorsAt
deleted def Simps.nsmulArgs:
added def Simps.nsmulArgs
modified def ToAdditive.etaExpandN
modified theorem mem_residual
modified theorem Set.einfsep_zero
modified theorem Bool_eq_iff2
modified theorem Bool_eq_iff
modified theorem lemma_with_false_in_head
modified theorem foo
deleted def two:
added def two
deleted def zero:
added def zero
modified theorem bar
added def nbhd