Skip to content

norm_num for Nat.factors #15410

@eric-wieser

Description

@eric-wieser

In lean 3 we had

https://github.com/leanprover-community/mathlib3/blob/65a1391a0106c9204fe45bc73a039f056558cb83/src/data/nat/prime_norm_num.lean#L158-L251

Probably this is no longer elegible for norm_num, but it would be eligible for a simproc.

Either we should revive the old code, or use a simpler strategy of computing the factors and showing that [2, 3, 3].prod = 12 by rfl.

Metadata

Metadata

Assignees

No one assigned

    Labels

    t-metaTactics, attributes or user commands

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions